`PosReal`

definition

show as: view math explainer →

module: IndisputableMonolith.Algebra.CostAlgebra
domain: Algebra
line: 732 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 732.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

 729    · simpa [h] using (J_reciprocal x hx).symm
 730
 731/-- The genuine positive domain of the canonical cost algebra. -/
 732abbrev PosReal := {x : ℝ // 0 < x}
 733
 734/-- Multiplication on positive reals. -/
 735def posMul (x y : PosReal) : PosReal :=
 736  ⟨x.1 * y.1, mul_pos x.2 y.2⟩
 737
 738/-- Inversion on positive reals. -/
 739noncomputable def posInv (x : PosReal) : PosReal :=
 740  ⟨x.1⁻¹, inv_pos.mpr x.2⟩
 741
 742/-- Distinguished positive constants used to close the automorphism proof. -/
 743def posOne : PosReal := ⟨1, by norm_num⟩
 744def posTwo : PosReal := ⟨2, by norm_num⟩
 745noncomputable def posHalf : PosReal := ⟨(1 / 2 : ℝ), by norm_num⟩
 746
 747@[simp] theorem posInv_inv (x : PosReal) : posInv (posInv x) = x := by
 748  apply Subtype.ext
 749  simp [posInv]
 750
 751@[simp] theorem posInv_one : posInv posOne = posOne := by
 752  apply Subtype.ext
 753  simp [posInv, posOne]
 754
 755@[simp] theorem posInv_two : posInv posTwo = posHalf := by
 756  apply Subtype.ext
 757  norm_num [posInv, posTwo, posHalf]
 758
 759@[simp] theorem posInv_half : posInv posHalf = posTwo := by
 760  apply Subtype.ext
 761  norm_num [posInv, posTwo, posHalf]
 762

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.