orderIsoRpow_symm_eq — Mathlib

English

The inverse of orderIsoRpow y hy equals orderIsoRpow (1/y) (one_div_pos.2 hy).

Русский

Обратное отображение orderIsoRpow y hy равно orderIsoRpow (1/y) с доказательством one_div_pos.

LaTeX

$$$\\forall y\\in\\mathbb{R},\\; hy>0:\\; (orderIsoRpow\ n y\ n).^{-1} = orderIsoRpow(1/y) (one\\_div\\_pos.2\; hy)$$$

Lean4

theorem orderIsoRpow_symm_eq (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

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