eq_sInf_of_mem_iff_exists_mem — Mathlib

English

If S ⊆ Filter α satisfies that s ∈ l iff ∃ f ∈ S, s ∈ f for all s, then l equals the infimum sInf S.

Русский

Пусть S ⊆ фильтров α удовлетворяет, что s ∈ l эквивалентно ∃ f ∈ S, s ∈ f для всех s; тогда l равно наибольшему нижнему пределу S.

LaTeX

$$$\forall l, (\forall s, s \in l \iff (\exists f \in S, s \in f)) \Rightarrow l = \sInf S$$$

Lean4

theorem eq_sInf_of_mem_iff_exists_mem {S : Set (Filter α)} {l : Filter α} (h : ∀ {s}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) :
    l = sInf S :=
  le_antisymm (le_sInf fun f hf _ hs => h.2 ⟨f, hf, hs⟩) fun _ hs =>
    let ⟨_, hf, hs⟩ := h.1 hs;
    (sInf_le hf) hs

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