eventually_sSup — Mathlib

English

The eventual property with respect to the supremum of a set of filters is equivalent to the universal property over the set.

Русский

Свойство, выполняющееся часто относительно sSup fs, эквивалентно для всех f ∈ fs, выполняющемуся часто для f.

LaTeX

$$$ (\forall^\infty x \in sSup\ fs,\ p x) \leftrightarrow \forall f \in fs, \forall^\infty x \in f,\ p x $$$

Lean4

@[simp]
theorem eventually_sSup {p : α → Prop} {fs : Set (Filter α)} : (∀ᶠ x in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ x in f, p x :=
  Iff.rfl

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