toENat_le_natCast_iff

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Cardinal.toENat_le_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) \leq n \;\iff\; c \leq n$$$

Lean4

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

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

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

Разделы

Аффилиация

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