nat_le_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

For every m ∈ ℕ and n ∈ ENat, the natural-number cardinal (m) is ≤ n iff m ≤ n.

Русский

Для всех m ∈ ℕ и n ∈ ENat выполняется, что (m : Cardinal) ≤ n тогда же, что и m ≤ n.

LaTeX

$$$\forall m : \mathbb{N}, \forall n : \mathbb{N}_\infty, (m : \mathrm{Cardinal}) \le n \iff m \le n$$$

Lean4

@[simp]
theorem nat_le_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n := by norm_cast

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

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

Разделы

Аффилиация

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