eventually_sup — Mathlib

English

Truth under the supremum of two filters is equivalent to truth under each filter separately.

Русский

Истина относительно суперфильтра f ⊔ g равна истине относительно каждого фильтра отдельно.

LaTeX

$$$ (\forall^\infty x \in f \oplus g,\ p x) \leftrightarrow (\forall^\infty x \in f,\ p x) \land (\forall^\infty x \in g,\ p x) $$$

Lean4

@[simp]
theorem eventually_sup {p : α → Prop} {f g : Filter α} : (∀ᶠ x in f ⊔ g, p x) ↔ (∀ᶠ x in f, p x) ∧ ∀ᶠ x in g, p x :=
  Iff.rfl

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