nhdsKer_inter_subset

Mathlib.Topology.NhdsKer

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

English

The kernel of the intersection equals the intersection of the kernels: nhdsKer(s ∩ t) ⊆ nhdsKer(s) ∩ nhdsKer(t).

Русский

Ядро пересечения равно пересечению ядер: nhdsKer(s ∩ t) ⊆ nhdsKer(s) ∩ nhdsKer(t).

LaTeX

$$$nhdsKer(s \\cap t) \\subseteq nhdsKer(s) \\cap nhdsKer(t)$$$

Lean4

theorem nhdsKer_inter_subset {s t : Set X} : nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t :=
  nhdsKer_mono.map_inf_le _ _

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

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

Разделы

Аффилиация

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