bUnion_mem_nhdsSet — Mathlib

English

Disjoint (nhdsSet s) (principal t) iff Disjoint (closure s) t.

Русский

Не пересекаются nhdsSet s и principal t тогда и только тогда, когда Disjoint(closure s, t).

LaTeX

$$$Disjoint (nhdsSet s) (Filter.principal t) \\iff Disjoint (closure s) t$$$

Lean4

theorem bUnion_mem_nhdsSet {t : X → Set X} (h : ∀ x ∈ s, t x ∈ 𝓝 x) : (⋃ x ∈ s, t x) ∈ 𝓝ˢ s :=
  mem_nhdsSet_iff_forall.2 fun x hx => mem_of_superset (h x hx) <| subset_iUnion₂ (s := fun x _ => t x) x hx

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