`toNat_lt`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 472 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 472.

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

depends on

used by

formal source

 469      exact h1
 470    exact this
 471
 472theorem toNat_lt (a b : LogicNat) : a < b ↔ toNat a < toNat b := by
 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) :=

papers checked against this theorem

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