ker_surjective — Mathlib

English

The map ker: Filter α → Set α is surjective onto all subsets of α; for every subset s ⊆ α there exists a filter f with ker f = s.

Русский

Функция ker: фильтры α → множества α покомплектна: для любой подмножества s ⊆ α найдётся фильтр f с ker f = s.

LaTeX

$$$\\forall S \\subseteq \\alpha, \\exists f : \\text{Filter } \\alpha, \\ker f = S$$$

Lean4

theorem ker_surjective : Surjective (ker : Filter α → Set α) :=
  gi_principal_ker.u_surjective

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