HelpersLib.PReal.Basic

source

@[reducible, inline]

abbrev PReal :

Type

Equations

ℝ>0 = { r : ℝ // 0 < r }

Instances For

source

def «termℝ>0» :

Lean.ParserDescr

Equations

«termℝ>0» = Lean.ParserDescr.node `«termℝ>0» 1024 (Lean.ParserDescr.symbol "ℝ>0")

Instances For

source

@[simp]

theorem add_toReal (x y : ℝ>0) :

↑(x + y) = ↑x + ↑y

source

def PReal.toReal :

ℝ>0 → ℝ

Equations

PReal.toReal = Subtype.val

Instances For

source

instance PReal.instCoeReal :

Coe ℝ>0 ℝ

Equations

PReal.instCoeReal = { coe := PReal.toReal }

source

def PReal.toNNReal :

ℝ>0 → NNReal

Equations

↑x = ⟨↑x, ⋯⟩

Instances For

source

instance PReal.instCoeNNReal :

Coe ℝ>0 NNReal

Equations

PReal.instCoeNNReal = { coe := PReal.toNNReal }

source

@[simp]

theorem PReal.val_eq_toNNReal (n : ℝ>0) :

↑n = ↑n

source

theorem PReal.toReal_pos (x : ℝ>0) :

0 < ↑x

source

theorem PReal.eq_iff_toReal_eq (x y : ℝ>0) :

x = y ↔ ↑x = ↑y

source

theorem PReal.toReal_ne_zero (x : ℝ>0) :

↑x ≠ 0

source

@[simp]

theorem PReal.toNNRealReal_eq_toNNReal (x : ℝ>0) :

↑↑x = ↑x

source

@[simp]

theorem PReal.toRealPReal_eq_toPReal (x : ℝ>0) :

⟨↑x, ⋯⟩ = x

source

theorem PReal.toNNReal_ne_zero (x : ℝ>0) :

↑x ≠ 0

source

theorem PReal.zero_lt_toNNReal (x : ℝ>0) :

0 < ↑x

source

@[simp]

theorem PReal.add_toReal (x y : ℝ>0) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem PReal.add_toNNReal (x y : ℝ>0) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem PReal.mul_toReal (x y : ℝ>0) :

↑(x * y) = ↑x * ↑y

source

@[simp]

theorem PReal.mul_toNNReal (x y : ℝ>0) :

↑(x * y) = ↑x * ↑y

source

@[simp]

theorem PReal.div_toReal (x y : ℝ>0) :

↑(x / y) = ↑x / ↑y

source

@[simp]

theorem PReal.div_toNNReal (x y : ℝ>0) :

↑(x / y) = ↑x / ↑y

source

@[simp]

theorem PReal.inv_toReal (x : ℝ>0) :

↑x⁻¹ = (↑x)⁻¹

source

@[simp]

theorem PReal.inv_toNNReal (x : ℝ>0) :

↑x⁻¹ = (↑x)⁻¹

source

theorem PReal.sq_toReal (x : ℝ>0) :

↑(x ^ 2) = ↑x ^ 2

source

theorem PReal.toReal_injective :

Function.Injective toReal

source

@[simp]

theorem PReal.toReal_eq_toReal_iff (x y : ℝ>0) :

x = y ↔ ↑x = ↑y

source

theorem PReal.toNNReal_injective :

Function.Injective toNNReal

source

theorem PReal.toNNReal_eq_toNNReal_iff (x y : ℝ>0) :

↑x = ↑y ↔ x = y

source

@[simp]

theorem PReal.toReal_le_toReal_iff (x y : ℝ>0) :

x ≤ y ↔ ↑x ≤ ↑y

source

theorem PReal.toNNReal_le_toNNReal_iff (x y : ℝ>0) :

x ≤ y ↔ ↑x ≤ ↑y

source

@[simp]

theorem PReal.toReal_lt_toReal_iff (x y : ℝ>0) :

x < y ↔ ↑x < ↑y

source

theorem PReal.toNNReal_lt_toNNReal_iff (x y : ℝ>0) :

↑x < ↑y ↔ x < y

source

@[simp]

theorem PReal.toReal_cmp (x y : ℝ>0) :

cmp x y = cmp ↑x ↑y

source

theorem PReal.toNNReal_cmp (x y : ℝ>0) :

cmp ↑x ↑y = cmp x y

source

theorem PReal.add_div'' {α : Type} [DivInvMonoid α] [Add α] [RightDistribClass α] (a b c : α) :

(a + b) / c = a / c + b / c

source

@[simp]

theorem PReal.mk_toReal (x : ℝ) (h : 0 < x) :

↑⟨x, h⟩ = x

source

@[simp]

theorem PReal.mk_toNNReal (x : ℝ) (h : 0 < x) :

↑⟨x, h⟩ = x.toNNReal

source

theorem PReal.toReal_one_eq_Real_one :

↑1 = 1