toENat_le_iff_of_le_aleph0

Mathlib.SetTheory.Cardinal.ENat

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

← MathLib Explorer

English

If c ≤ ℵ₀ and c' arbitrary, then toENat c ≤ toENat c' iff c ≤ c'.

Русский

Пусть c ≤ ℵ₀; тогда toENat c ≤ toENat c' тогда же, что и c ≤ c'.

LaTeX

$$$\\text{If } c \\le \\aleph_0:\\; toENat(c) \\le toENat(c') \\iff c \\le c'$$$

Lean4

theorem toENat_le_iff_of_le_aleph0 {c c' : Cardinal} (h : c ≤ ℵ₀) : toENat c ≤ toENat c' ↔ c ≤ c' :=
  by
  lift c to ℕ∞ using h
  simp_rw [toENat_ofENat, enat_gc _]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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