of_injective_continuous — Mathlib

English

If f: X→Y is injective and continuous and Y is a T25-space, then X is T25-space.

Русский

Если отображение f: X→Y инъективно и непрерывно, а Y - T25-пространство, то X also является T25-пространством.

LaTeX

$$$[T25Space Y]\; (\text{Injective } f)\; (\text{Continuous } f) \Rightarrow T25Space X.$$$

Lean4

theorem of_injective_continuous [TopologicalSpace Y] [T25Space Y] {f : X → Y} (hinj : Injective f)
    (hcont : Continuous f) : T25Space X where
  t2_5 x y
    hne := (tendsto_lift'_closure_nhds hcont x).disjoint (t2_5 <| hinj.ne hne) (tendsto_lift'_closure_nhds hcont y)

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