pith. machine review for the scientific record. sign in
theorem proved tactic proof

toNat_lt

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)

 472theorem toNat_lt (a b : LogicNat) : a < b ↔ toNat a < toNat b := by

proof body

Tactic-mode proof.

 473  rw [lt_iff_succ_le, toNat_le]
 474  constructor
 475  · intro h
 476    rw [toNat_succ] at h
 477    omega
 478  · intro h
 479    rw [toNat_succ]
 480    omega
 481
 482/-- `LogicNat` is a linear order: any two elements are comparable, and
 483the order is decidable. Both follow from the recovery isomorphism with
 484`Nat`. -/
 485instance : LinearOrder LogicNat where
 486  __ := (inferInstance : PartialOrder LogicNat)
 487  le_total := fun a b => by
 488    rcases Nat.le_total (toNat a) (toNat b) with h | h
 489    · left
 490      exact (toNat_le a b).mpr h
 491    · right
 492      exact (toNat_le b a).mpr h
 493  toDecidableLE := fun a b =>
 494    decidable_of_iff (toNat a ≤ toNat b) (toNat_le a b).symm
 495  toDecidableEq := inferInstance
 496
 497/-- `LogicNat` is well-founded under strict order: induction on size is
 498admissible. Transfer from `Nat`'s well-foundedness via the recovery
 499isomorphism. -/
 500instance : WellFoundedLT LogicNat where
 501  wf := by
 502    have hNat : WellFounded (fun a b : LogicNat => toNat a < toNat b) :=
 503      InvImage.wf toNat (Nat.lt_wfRel.wf)
 504    apply Subrelation.wf (h₁ := ?_) hNat
 505    intro a b h
 506    exact (toNat_lt a b).mp h
 507
 508end LogicNat
 509
 510/-! ## 6. Embedding into ℝ₊ via a Generator
 511
 512Section 5 recovers the abstract Peano structure. Section 6 ties that

used by (2)

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

depends on (16)

Lean names referenced from this declaration's body.