nhdsKer_iInter_subset — Mathlib

English

For any family of sets {s_i}, the kernel of the intersection is contained in the intersection of the kernels.

Русский

Для любого семейства множеств {s_i} ядро пересечения удовлетворяет ⊆ пересечению ядер множеств: nhdsKer(⋂ i, s_i) ⊆ ⋂ i, nhdsKer(s_i).

LaTeX

$$$nhdsKer(\\bigcap_i s_i) \\subseteq \\bigcap_i nhdsKer(s_i)$$$

Lean4

theorem nhdsKer_iInter_subset {s : ι → Set X} : nhdsKer (⋂ i, s i) ⊆ ⋂ i, nhdsKer (s i) :=
  nhdsKer_mono.map_iInf_le

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