toENat_eq_iff_of_le_aleph0

Mathlib.SetTheory.Cardinal.ENat

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

← MathLib Explorer

English

For c,c' ≤ ℵ₀, toENat c = toENat c' implies c=c'.

Русский

Для c, c' ≤ ℵ₀: toENat c = toENat c' → c=c'.

LaTeX

$$$c \\le \\aleph_0 \\land c' \\le \\aleph_0 \\Rightarrow (toENat c = toENat c' \\iff c = c')$$$

Lean4

theorem toENat_eq_iff_of_le_aleph0 {c c' : Cardinal} (hc : c ≤ ℵ₀) (hc' : c' ≤ ℵ₀) : toENat c = toENat c' ↔ c = c' :=
  toENat_strictMonoOn.injOn.eq_iff hc hc'

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

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

Разделы

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

Аффилиация

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