eq_top_iff_forall_lt — Mathlib

English

An element x of PartENat equals the top if and only if every natural number cast into PartENat is strictly less than x.

Русский

Элемент x PartENat равен верхнему, если и только если каждый натуральный n, приведённый к PartENat, строго меньше x.

LaTeX

$$$ x = \top \iff \forall n : \mathbb{N}, (n : \mathrm{PartENat}) < x $$$

Lean4

theorem eq_top_iff_forall_lt (x : PartENat) : x = ⊤ ↔ ∀ n : ℕ, (n : PartENat) < x :=
  by
  constructor
  · rintro rfl n
    exact natCast_lt_top _
  · contrapose!
    rw [ne_top_iff]
    rintro ⟨n, rfl⟩
    exact ⟨n, irrefl _⟩

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