nhdsKer_union

Mathlib.Topology.NhdsKer

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

English

nhdsKer(s ∪ t) = nhdsKer(s) ∪ nhdsKer(t).

Русский

nhdsKer(s ∪ t) = nhdsKer(s) ∪ nhdsKer(t).

LaTeX

$$nhdsKer(s ∪ t) = nhdsKer(s) ∪ nhdsKer(t)$$

Lean4

@[simp]
theorem nhdsKer_union (s t : Set X) : nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t := by
  simp only [nhdsKer, nhdsSet_union, ker_sup]

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

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

Разделы

Аффилиация

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