powerlt_le_powerlt_left

Mathlib.SetTheory.Cardinal.Basic

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

English

For cardinals a, b, c, if b ≤ c then a^{<b} ≤ a^{<c}.

Русский

Пусть кардиналы a, b, c удовлетворяют b ≤ c; тогда a^{<b} ≤ a^{<c}.

LaTeX

$$$b \\le c \\Rightarrow a^{< b} \\le a^{< c}$$$

Lean4

theorem powerlt_le_powerlt_left {a b c : Cardinal} (h : b ≤ c) : a ^< b ≤ a ^< c :=
  powerlt_le.2 fun _ hx => le_powerlt a <| hx.trans_le h

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

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

Разделы

Аффилиация

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