toENat_eq_natCast_iff

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Cardinal.toENat_eq_natCast_iff

English

For any cardinal c and natural n,.toENat c = n iff c = n.

Русский

Для любого кардинала c и натурального n, toENat c = n тогда и только тогда, когда c = n.

LaTeX

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

Lean4

theorem _root_.Cardinal.toENat_eq_natCast_iff {c : Cardinal} {n : ℕ} : Cardinal.toENat c = n ↔ c = n := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru