orderIsoRpow_symm_apply — Mathlib

English

The symmetrized form: (orderIsoRpow y hy).symm = orderIsoRpow (1/y) (one_div_pos.2 hy).

Русский

Симметрированная форма: (orderIsoRpow y hy).symm = orderIsoRpow (1/y) (one_div_pos.2 hy).

LaTeX

$$$$(\text{orderIsoRpow } y\; \text{hy}).\text{symm} = \text{orderIsoRpow}(1/y)\,(\text{one_div_pos.2 hy}).$$$$

Lean4

theorem orderIsoRpow_symm_apply (y : ℝ) (hy : 0 < y) :
    (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) (one_div_pos.2 hy) :=
  by
  simp only [orderIsoRpow, one_div_one_div]
  rfl

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