frequently_smallSets' — Mathlib

English

If p is monotone with respect to inclusion, then frequent p on l.smallSets is equivalent to p holding for all t ∈ l.

Русский

Если p монотонно по включению, то частотность p на l.smallSets эквивалентна тому, что p выполняется для всех t ∈ l.

LaTeX

$$$ (\\\\forall ⦃s t⦄, s \\subseteq t \\to p(t) \\to p(s)) \\\\Rightarrow (\\\\exists^\\\\infty s \\\\in l.smallSets, p(s)) \\\\iff \\\\forall t \\\\in l, p(t) $$

Lean4

theorem frequently_smallSets' {α : Type*} {l : Filter α} {p : Set α → Prop} (hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t) :
    (∃ᶠ s in l.smallSets, p s) ↔ ∀ t ∈ l, p t :=
  by
  convert not_iff_not.mpr <| l.eventually_smallSets' (p := (¬p ·)) (by tauto)
  simp

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