natCast_lt_toENat_iff — Mathlib

English

For any n ∈ ℕ and c ∈ Cardinal, ↑n < toENat c iff ↑n < c.

Русский

Для любых n ∈ ℕ и кардинала c, n как ENat < toENat(c) тогда и только тогда, когда n < c.

LaTeX

$$$\uparrow n < \operatorname{toENat}(c) \;\iff\; \uparrow n < c$$$

Lean4

@[simp]
theorem _root_.Cardinal.natCast_lt_toENat_iff {n : ℕ} {c : Cardinal} : ↑n < toENat c ↔ ↑n < c := by
  simp only [← not_le, Cardinal.toENat_le_natCast_iff]

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