toOrderIso — Mathlib

English

The underlying function of toOrderIso f equals f.

Русский

Функция, лежащая в основе toOrderIso f, равна f.

LaTeX

$$$\\iota(f) = f$ where $\\iota$ denotes the underlying function of toOrderIso$$

Lean4

/-- If a lift of a circle map is bijective, then it is an order automorphism of the line. -/
def toOrderIso : CircleDeg1Liftˣ →* ℝ ≃o ℝ
    where
  toFun
    f :=
    { toFun := f
      invFun := ⇑f⁻¹
      left_inv := units_inv_apply_apply f
      right_inv := units_apply_inv_apply f
      map_rel_iff' := ⟨fun h => by simpa using mono (↑f⁻¹) h, mono f⟩ }
  map_one' := rfl
  map_mul' _ _ := rfl

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