of_hasBasis — Mathlib

English

More generally, if for each x the neighborhood filter has a HasBasis by closed sets, then RegularSpace X holds.

Русский

Более общо, если локальная структура окрестностей имеет базис по замкнутым отображениям, то пространство регулярное.

LaTeX

$$$\\text{RegularSpace}(X)$ from HasBasis of nbhd by closed sets$$

Lean4

theorem of_hasBasis {ι : X → Sort*} {p : ∀ a, ι a → Prop} {s : ∀ a, ι a → Set X} (h₁ : ∀ a, (𝓝 a).HasBasis (p a) (s a))
    (h₂ : ∀ a i, p a i → IsClosed (s a i)) : RegularSpace X :=
  .of_lift'_closure fun a => (h₁ a).lift'_closure_eq_self (h₂ a)

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