eventually_smallSets_forall — Mathlib

English

The universal statement over smallSets is equivalent to eventual universality over the base filter.

Русский

Универсальное утверждение над smallSets эквивалентно универсальности вдоль базового фильтра.

LaTeX

$$$ (\\\\forall^\\\\infty s \\\\in l.smallSets, \\\\forall x \\\\in s, p(x)) \\\\iff \\\\forall^\\\\infty x \\\\in l, p(x) $$$

Lean4

@[simp]
theorem eventually_smallSets_forall {p : α → Prop} : (∀ᶠ s in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ x in l, p x := by
  simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

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