instTietzeExtension — Mathlib

English

Any homeomorphism from a TietzeExtension space is itself a TietzeExtension space.

Русский

Любой гомеоморфизм из пространства TietzeExtension само является пространством TietzeExtension.

LaTeX

$$$\\forall e:\\ Y \\simeq_t Z,\\ [\\mathrm{TietzeExtension}(Z)] \\Rightarrow \\mathrm{TietzeExtension}(Y)$$$

Lean4

instance instTietzeExtension {Y : Type v} [TopologicalSpace Y] [Nonempty Y] [Subsingleton Y] : TietzeExtension.{u, v} Y
    where exists_restrict_eq' _ _ f := ‹Nonempty Y›.elim fun y ↦ ⟨.const _ y, by ext; subsingleton⟩

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