beth_mono

Mathlib.SetTheory.Cardinal.Aleph

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

English

The beth function is monotone (order-preserving): if o1 ≤ o2 then beth(o1) ≤ beth(o2).

Русский

Функция beth монотонна: если o1 ≤ o2, то beth(o1) ≤ beth(o2).

LaTeX

$$$\beth(o_1) \le \beth(o_2) \iff o_1 \le o_2$$$

Lean4

theorem beth_mono : Monotone beth :=
  beth_strictMono.monotone

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

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

Разделы

Аффилиация

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