nhdsKer_sInter_subset — Mathlib

English

The kernel of the intersection over a set s of subsets is contained in the intersection over all members of s of their kernels.

Русский

Ядро пересечения ⋂₀ s содержится в пересечении по всем элементам s их ядер.

LaTeX

$$$nhdsKer(\\bigcap_0 s) \\subseteq \\bigcap x \\in s, nhdsKer(x)$$$

Lean4

theorem nhdsKer_sInter_subset {s : Set (Set X)} : nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x :=
  nhdsKer_mono.map_sInf_le

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