toNat_injOn

Mathlib.SetTheory.Cardinal.ToNat

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

English

If c and d are finite cardinals (c < aleph0 and d < aleph0) and toNat(c) = toNat(d), then c = d.

Русский

Если c и d — конечные кардиналы (c < ℵ0 и d < ℵ0) и toNat(c) = toNat(d), то c = d.

LaTeX

$$$\forall c,d \in Iio(\aleph_0): \operatorname{toNat}(c) = \operatorname{toNat}(d) \Rightarrow c = d.$$$

Lean4

theorem toNat_injOn : InjOn toNat (Iio ℵ₀) :=
  toNat_strictMonoOn.injOn

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

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

Разделы

Аффилиация

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