eq_top_iff_forall_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem eq_top_iff_forall_le (x : PartENat) : x = ⊤ ↔ ∀ n : ℕ, (n : PartENat) ≤ x :=
  (eq_top_iff_forall_lt x).trans
    ⟨fun h n => (h n).le, fun h n => lt_of_lt_of_le (coe_lt_coe.mpr n.lt_succ_self) (h (n + 1))⟩

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