orderIsoIicOneBirational_symm_apply

English

For x ∈ Iic(1), the inverse map satisfies orderIsoIicOneBirational.symm x = (x.1⁻¹ - 1)⁻¹.

Русский

Для x ∈ Iic(1) обратная карта удовлетворяет orderIsoIicOneBirational.symm x = (x.1⁻¹ - 1)⁻¹.

LaTeX

$$$$ \mathrm{orderIsoIicOneBirational}.\mathrm{symm}(x) = (x.1^{-1} - 1)^{-1}. $$$$

Lean4

@[simp]
theorem orderIsoIicOneBirational_symm_apply (x : Iic (1 : ℝ≥0∞)) : orderIsoIicOneBirational.symm x = (x.1⁻¹ - 1)⁻¹ :=
  rfl

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