powerlt_mono_left

Mathlib.SetTheory.Cardinal.Basic

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

English

For a fixed a, the function c ↦ a^{<c} is monotone; i.e., if c ≤ d then a^{<c} ≤ a^{<d}.

Русский

Для фиксированного a отображение c ↦ a^{<c} монотонно: если c ≤ d, то a^{<c} ≤ a^{<d}.

LaTeX

$$∀ {a : Cardinal}, Monotone (fun c => a^{< c})$$

Lean4

theorem powerlt_mono_left (a) : Monotone fun c => a ^< c := fun _ _ => powerlt_le_powerlt_left

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

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

Разделы

Аффилиация

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