toENatAux_le_nat — Mathlib

English

For any cardinal x and natural number n, the comparison via toENatAux respects nat-bounds: toENatAux(x) ≤ n iff x ≤ n.

Русский

Для любого кардинала x и нат. число n сравнение через toENatAux совпадает с обычным x ≤ n.

LaTeX

$$$\\forall x \\in \\mathrm{Cardinal},\\ \\forall n \\in \\mathbb{N},\\ toENatAux(x) \\le n \\iff x \\le n$$$

Lean4

theorem toENatAux_le_nat {x : Cardinal} {n : ℕ} : toENatAux x ≤ n ↔ x ≤ n := by
  cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (nat_lt_aleph0 n).trans_le hx]

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