pith. machine review for the scientific record. sign in
def definition def or abbrev

positiveRatioOrbitInterpret

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  86noncomputable def positiveRatioOrbitInterpret
  87    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  88    LogicNat → {x : ℝ // 0 < x}
  89  | LogicNat.identity => ⟨1, one_pos⟩
  90  | LogicNat.step n =>
  91      let γ : ℝ := Classical.choose h.non_trivial

proof body

Definition body.

  92      let x := positiveRatioOrbitInterpret C h n
  93      ⟨γ * x.1, mul_pos (Classical.choose_spec h.non_trivial).1 x.2⟩
  94

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.