homeomorph — Mathlib

English

If α is endowed with the Lawson topology, then there exists a natural homeomorphism between WithLawson α and α.

Русский

Если альфе задана топология Lawson, то существует естественный гомеоморфизм между WithLawson α и α.

LaTeX

$$$\mathrm{WithLawson}\;\alpha \cong_t \alpha$$$

Lean4

/-- If `α` is equipped with the Lawson topology, then it is homeomorphic to `WithLawson α`.
-/
def homeomorph [TopologicalSpace α] [IsLawson α] : WithLawson α ≃ₜ α :=
  ofLawson.toHomeomorphOfIsInducing ⟨IsLawson.topology_eq_lawson (α := α) ▸ induced_id.symm⟩

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