toENatAux_eq_top — Mathlib

English

Any cardinal a with size at least that of the natural numbers (i.e., a ≥ ℵ0) maps to the top element ⊤ in ENat under toENatAux.

Русский

Любое кардинальное число a с размером не меньше ℵ0 отображается в верхнюю точку ⊤ ENat под toENatAux.

LaTeX

$$$\\aleph_0 \\le a \\;\\Rightarrow\\; \\operatorname{toENatAux}(a) = \\top$$$

Lean4

theorem toENatAux_eq_top {a : Cardinal} (ha : ℵ₀ ≤ a) : toENatAux a = ⊤ :=
  extend_apply' _ _ _ fun ⟨n, hn⟩ ↦ ha.not_gt <| hn ▸ nat_lt_aleph0 n

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