natCast_eq_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_eq_toENat_iff {n : ℕ} {c : Cardinal} : ↑n = toENat c ↔ ↑n = c := by
  rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast_iff, Cardinal.natCast_le_toENat_iff]

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