ofComplNotMemIff — Mathlib

English

If a filter f satisfies s^c ∉ f ↔ s ∈ f for all s, then one can form an ultrafilter from f.

Русский

Если фильтр f удовлетворяет s^c ∉ f ↔ s ∈ f для всех s, то из f можно получить ульрафильтр.

LaTeX

$$$\\\\mathrm{ofComplNotMemIff} : \\\\mathrm{Filter}(\\\\alpha) \\\\to (\\\\forall s, s^c ∉ f \\\\Leftrightarrow s ∈ f) \\\\to \\\\mathrm{Ultrafilter}(\\\\alpha)$$$

Lean4

/-- If `sᶜ ∉ f ↔ s ∈ f`, then `f` is an ultrafilter. The other implication is given by
`Ultrafilter.compl_notMem_iff`. -/
def ofComplNotMemIff (f : Filter α) (h : ∀ s, sᶜ ∉ f ↔ s ∈ f) : Ultrafilter α
    where
  toFilter := f
  neBot' := ⟨fun hf => by simp [hf] at h⟩
  le_of_le _ _ hgf s hs := (h s).1 fun hsc => compl_notMem hs (hgf hsc)

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