eventually_smallSets_subset — Mathlib

English

Let l be a filter on a set α and s a subset of α. Then almost every t in l.smallSets satisfies t ⊆ s if and only if s ∈ l.

Русский

Пусть l — фильтр на множество α, и Пусть s ⊆ α. Тогда почти наверняка для t из l.smallSets выполняется t ⊆ s тогда и только тогда, когда s принадлежит l.

LaTeX

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

Lean4

@[simp]
theorem eventually_smallSets_subset {s : Set α} : (∀ᶠ t in l.smallSets, t ⊆ s) ↔ s ∈ l :=
  eventually_smallSets_forall

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