nat_lt

Mathlib.SetTheory.Cardinal.Regular

URI: https://scilib.ai/kg/mathlib#Cardinal.IsRegular.nat_lt

English

For every natural n and regular cardinal c, n < c.

Русский

Для каждого натурального числа n и регулярного кардинала c верно n < c.

LaTeX

$$$\forall n \in \mathbb{N},\ n < c.$$$

Lean4

theorem nat_lt {c : Cardinal} (H : c.IsRegular) (n : ℕ) : n < c :=
  lt_of_lt_of_le (nat_lt_aleph0 n) H.aleph0_le

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

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

Разделы

Аффилиация

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