toENat_injOn

Mathlib.SetTheory.Cardinal.ENat

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

English

The restriction of toENat to the finite cardinals (≤ ℵ0) is injective.

Русский

Ограничение toENat на конечные кардиналы (≤ ℵ0) инъективно.

LaTeX

$$$\\operatorname{InjOn}(\\operatorname{toENat}, \\mathrm{Iic}(\\aleph_0))$$$

Lean4

theorem toENat_injOn : InjOn toENat (Iic ℵ₀) :=
  toENat_strictMonoOn.injOn

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

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

Разделы

Аффилиация

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