ker_inf

Mathlib.Order.Filter.Ker

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

English

The kernel of the infimum (greatest lower bound) of f and g equals the intersection of their kernels: ker (f ⊓ g) = ker f ∩ ker g.

Русский

Ядро inf{f,g} равно пересечению ядер f и g: ker (f ⊓ g) = ker f ∩ ker g.

LaTeX

$$$\\ker(f \\sqcap g) = \\ker f \\cap \\ker g$$$

Lean4

@[simp]
theorem ker_inf (f g : Filter α) : ker (f ⊓ g) = ker f ∩ ker g :=
  gi_principal_ker.gc.u_inf

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

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

Разделы

Аффилиация

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