beth_strictMono

Mathlib.SetTheory.Cardinal.Aleph

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

English

The beth function is strictly increasing: if o1 < o2 then beth(o1) < beth(o2).

Русский

Функция beth строго возрастает: если o1 < o2, то beth(o1) < beth(o2).

LaTeX

$$$\text{StrictMono}(\mathrm{beth})(o_1, o_2) \iff o_1 < o_2 \text{ implies } \beth(o_1) < \beth(o_2)$$$

Lean4

theorem beth_strictMono : StrictMono beth :=
  preBeth_strictMono.comp fun _ _ h ↦ add_lt_add_left h _

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

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

Разделы

Аффилиация

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