lt_find_iff — Mathlib

English

For x, y in ENat, we have x < y iff the symmetric image respects LT: withTopEquiv.symm x < withTopEquiv.symm y ↔ x < y.

Русский

Для x, y ∈ ENat верно x < y тогда и только тогда, когда симметричное отображение сохраняет порядок: withTopEquiv.symm x < withTopEquiv.symm y ↔ x < y.

LaTeX

$$$ \forall {x,y : \mathrm{ENat}},\; withTopEquiv.symm x < withTopEquiv.symm y \iff x < y $$$

Lean4

theorem lt_find_iff (n : ℕ) : (n : PartENat) < find P ↔ ∀ m ≤ n, ¬P m :=
  by
  refine ⟨?_, lt_find P n⟩
  intro h m hm
  by_cases H : (find P).Dom
  · apply Nat.find_min H
    rw [coe_lt_iff] at h
    specialize h H
    exact lt_of_le_of_lt hm h
  · exact not_exists.mp H m

Похожие утверждения