t5Space — Mathlib

English

If e: X → Y is an embedding and Y is T5, then X is T5.

Русский

Если e: X → Y — вложение и Y — T5, тогда X — T5.

LaTeX

$$$ \\forall e: X \\to Y, \\ IsEmbedding(e) \\Rightarrow ( [T5Space Y] \\Rightarrow [T5Space X] )$$$

Lean4

theorem t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : IsEmbedding e) : T5Space X
    where
  __ := he.t1Space
  completely_normal := by
    have := he.completelyNormalSpace
    exact completely_normal

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