nhdsKer_iUnion

Mathlib.Topology.NhdsKer

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

English

nhdsKer of a union over an index set equals the union of nhdsKers.

Русский

nhdsKer объединения по индексу равен объединению nhdsKer по каждому элементу.

LaTeX

$$nhdsKer (⋃ i, s i) = ⋃ i, nhdsKer(s i)$$

Lean4

@[simp]
theorem nhdsKer_iUnion (s : ι → Set X) : nhdsKer (⋃ i, s i) = ⋃ i, nhdsKer (s i) := by
  simp only [nhdsKer, nhdsSet_iUnion, ker_iSup]

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

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

Разделы

Аффилиация

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