toHomeomorph — Mathlib

English

If g and f are homeomorphisms, then g ∘ f is a homeomorphism.

Русский

Если g и f — гомеоморфизмы, то их композиция g ∘ f — гомеоморфизм.

LaTeX

$$$ \\text{IsHomeomorph } g \\to\\text{IsHomeomorph } f \\to \\text{IsHomeomorph } (g \\circ f) $$$

Lean4

/-- Turn an element of a type `F` satisfying `HomeomorphClass F α β` into an actual
`Homeomorph`. This is declared as the default coercion from `F` to `α ≃ₜ β`. -/
@[coe]
def toHomeomorph [h : HomeomorphClass F α β] (f : F) : α ≃ₜ β :=
  { (f : α ≃ β) with
    continuous_toFun := h.map_continuous f
    continuous_invFun := h.inv_continuous f }

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