rpow_le_rpow_of_exponent_ge — Mathlib

English

In any linear order, for all a,b, b < a is equivalent to not (a ≤ b).

Русский

В любом линейном порядке для любых a, b выполняется: b < a тогда и только тогда, когда не (a ≤ b).

LaTeX

$$In any linear order, ∀ a,b, b < a ⇔ ¬(a ≤ b).$$

Lean4

theorem rpow_le_rpow_of_exponent_ge {x : ℝ≥0∞} {y z : ℝ} (hx1 : x ≤ 1) (hyz : z ≤ y) : x ^ y ≤ x ^ z :=
  by
  lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx1 coe_lt_top)
  by_cases h : x = 0
  ·
    rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;> rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
        simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos, le_refl] <;>
      linarith
  · rw [coe_le_one_iff] at hx1
    simp [← coe_rpow_of_ne_zero h, NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

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