mul_omega0_opow_opow — Mathlib

English

If a > 0 and a < ω^(ω^b), then a * ω^(ω^b) = ω^(ω^b).

Русский

Если a > 0 и a < ω^(ω^b), то a * ω^(ω^b) = ω^(ω^b).

LaTeX

$$$(0 < a) \land (a < \omega^{\omega^b}) \Rightarrow a * \omega^{\omega^b} = \omega^{\omega^b}.$$$

Lean4

theorem mul_omega0_opow_opow (a0 : 0 < a) (h : a < ω ^ ω ^ b) : a * ω ^ ω ^ b = ω ^ ω ^ b :=
  by
  obtain rfl | b0 := eq_or_ne b 0
  · rw [opow_zero, opow_one] at h ⊢
    exact mul_omega0 a0 h
  · apply le_antisymm
    · obtain ⟨x, xb, ax⟩ := (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h
      apply (mul_le_mul_right' (le_of_lt ax) _).trans
      rw [← opow_add, add_omega0_opow xb]
    · conv_lhs => rw [← one_mul (ω ^ _)]
      exact mul_le_mul_right' (one_le_iff_pos.2 a0) _

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