support_eq_univ_iff — Mathlib

English

A summation filter L has support equal to univ iff L.filter ≤ atTop.

Русский

Поддержка L равна целому множеству тогда и только тогда, когда L.filter ≤ atTop.

LaTeX

$$$ \text{support }(L) = \text{univ} \iff L.filter \leq atTop$$$

Lean4

theorem support_eq_univ_iff {L : SummationFilter β} : L.support = univ ↔ L.filter ≤ atTop :=
  by
  simp only [support, Set.eq_univ_iff_forall, Set.mem_setOf]
  refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩
  · obtain ⟨t, ht⟩ := mem_atTop_sets.mp hs
    have := (Filter.biInter_finset_mem t).mpr fun b hb ↦ h b
    exact Filter.mem_of_superset this fun r hr ↦ ht r (by simpa using hr)
  · filter_upwards [eventually_ge_atTop { b }] using by simp

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