frequently_smallSets — Mathlib

English

There are frequently small sets in l with property p if and only if for every t ∈ l there exists s ⊆ t with p(s).

Русский

Существуют частые малые множества в l с свойством p тогда и только тогда, когда для каждого t ∈ l существует s ⊆ t с p(s).

LaTeX

$$$ (\\\\exists^\\\\infty s \\\\in l.smallSets, p(s)) \\\\iff \\\\forall t \\\\in l, \\\\exists s, s \\\\subseteq t \\\\land p(s) $$$

Lean4

theorem frequently_smallSets {p : Set α → Prop} : (∃ᶠ s in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s, s ⊆ t ∧ p s :=
  l.hasBasis_smallSets.frequently_iff

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