ker_sSup

Mathlib.Order.Filter.Ker

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

English

The kernel distributes over supremum of a set: ker (sSup S) = ⋃ f ∈ S, ker f.

Русский

Ядро верхней границы множества фильтров распределяется: ker (sSup S) = ⋃ f ∈ S, ker f.

LaTeX

$$$\\ker(\\mathrm{sSup}\\,S) = \\bigcup_{f \\in S} \\ker f$$$

Lean4

@[simp]
theorem ker_sSup (S : Set (Filter α)) : ker (sSup S) = ⋃ f ∈ S, ker f := by simp [sSup_eq_iSup]

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

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

Разделы

Аффилиация

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