ker_eq_univ

Mathlib.Order.Filter.Ker

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

English

The kernel of f equals the universe if and only if f is the top filter.

Русский

Ядро фильтра f равно вселенному множеству тогда и только тогда, когда f = ⊤.

LaTeX

$$$\\ker f = \\univ \\iff f = \\top$$$

Lean4

@[simp]
theorem ker_eq_univ : ker f = univ ↔ f = ⊤ :=
  gi_principal_ker.gc.u_eq_top.trans <| by simp

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

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

Разделы

Аффилиация

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