`PosReal`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 732.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.