of_continuous_specializes_imp — Mathlib

English

If f: Y → X is continuous and reflects specialization, and X is R1, then Y is R1.

Русский

Если отображение f: Y → X непрерывно и сохраняет отношение specialise, и X — R1-пространство, то Y — R1-пространство.

LaTeX

$$R1Space_Y$$

Lean4

theorem of_continuous_specializes_imp [TopologicalSpace Y] {f : Y → X} (hc : Continuous f)
    (hspec : ∀ x y, f x ⤳ f y → x ⤳ y) : R1Space Y where
  specializes_or_disjoint_nhds x
    y := (specializes_or_disjoint_nhds (f x) (f y)).imp (hspec x y) <| ((hc.tendsto _).disjoint · (hc.tendsto _))

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