power_le_power_right

Mathlib.SetTheory.Cardinal.Order

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

English

If a ≤ b then a^c ≤ b^c for cardinals a,b,c.

Русский

Если a ≤ b, то a^c ≤ b^c для кардиналов a,b,c.

LaTeX

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

Lean4

theorem power_le_power_right {a b c : Cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
  inductionOn₃ a b c fun _ _ _ ⟨e⟩ => ⟨Embedding.arrowCongrRight e⟩

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

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

Разделы

Аффилиация

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