power_le_power_left

Mathlib.SetTheory.Cardinal.Order

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

← MathLib Explorer

English

If a ≠ 0 and b ≤ c then a^b ≤ a^c.

Русский

Если a ≠ 0 и b ≤ c, то a^b ≤ a^c.

LaTeX

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

Lean4

theorem power_le_power_left : ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
  by
  rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩
  let ⟨a⟩ := mk_ne_zero_iff.1 hα
  exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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