tanOrderIso — Mathlib

English

The tangent function provides an order isomorphism between the open interval (-π/2, π/2) and ℝ.

Русский

Тангенс задаёт порядкаизоморфизм между открытым интервалом (-π/2, π/2) и ℝ.

LaTeX

$$$ \text{tanOrderIso} : \mathrm{Ioo}(-\frac{\pi}{2}, \frac{\pi}{2}) \simeq_o \mathbb{R} $$$

Lean4

/-- `Real.tan` as an `OrderIso` between `(-(π / 2), π / 2)` and `ℝ`. -/
def tanOrderIso : Ioo (-(π / 2)) (π / 2) ≃o ℝ :=
  (strictMonoOn_tan.orderIso _ _).trans <| (OrderIso.setCongr _ _ image_tan_Ioo).trans OrderIso.Set.univ

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