completelyRegularSpace — Mathlib

English

If X is completely regular, then any subspace defined by a predicate p is completely regular.

Русский

Если X полностью регулярное, то любое подпопство, заданное предикатом p, также полностью регулярное.

LaTeX

$$$[CompletelyRegularSpace X] \\Rightarrow [CompletelyRegularSpace (Subtype p)]$$$

Lean4

theorem completelyRegularSpace {Y : Type v} [TopologicalSpace Y] [CompletelyRegularSpace Y] {f : X → Y}
    (hf : IsInducing f) : CompletelyRegularSpace X where
  completely_regular x K hK
    hxK := by
    rw [hf.isClosed_iff] at hK
    obtain ⟨K, hK, rfl⟩ := hK
    rw [mem_preimage] at hxK
    obtain ⟨g, hcf, egfx, hgK⟩ := CompletelyRegularSpace.completely_regular _ _ hK hxK
    refine ⟨g ∘ f, hcf.comp hf.continuous, egfx, ?_⟩
    conv => arg 2; equals (1 : Y → ↥I) ∘ f => rfl
    exact hgK.comp_right <| mapsTo_preimage _ _

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