nhdsKer_sUnion

Mathlib.Topology.NhdsKer

URI: https://scilib.ai/kg/mathlib#nhdsKer_sUnion

English

nhdsKer of a sUnion equals the union of nhdsKers over all members.

Русский

nhdsKer ⋃S равно ⋃s∈S nhdsKer(s).

LaTeX

$$nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s$$

Lean4

@[simp]
theorem nhdsKer_sUnion (S : Set (Set X)) : nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s := by
  simp only [sUnion_eq_biUnion, nhdsKer_iUnion]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru