ker_sup

Mathlib.Order.Filter.Ker

URI: https://scilib.ai/kg/mathlib#Filter.ker_sup

English

The kernel of the supremum (join) of f and g is the union of the kernels: ker (f ⊔ g) = ker f ∪ ker g.

Русский

Ядро объединения филтров f и g равно объединению их ядер: ker(f ⊔ g) = ker f ∪ ker g.

LaTeX

$$$\\ker(f \\sqcup g) = \\ker f \\cup \\ker g$$$

Lean4

@[simp]
theorem ker_sup (f g : Filter α) : ker (f ⊔ g) = ker f ∪ ker g := by rw [← sSup_pair, ker_sSup, biUnion_pair]

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

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

Разделы

Аффилиация

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