ker_mono

Mathlib.Order.Filter.Ker

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

English

The kernel operation ker: Filter α → Set α is monotone: if f ≤ g then ker f ⊆ ker g.

Русский

Операция ядра монотонна: если f ≤ g, то ker f ⊆ ker g.

LaTeX

$$$f \\le g \\Rightarrow \\ker f \\subseteq \\ker g$$$

Lean4

theorem ker_mono : Monotone (ker : Filter α → Set α) :=
  gi_principal_ker.gc.monotone_u

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

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

Разделы

Аффилиация

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