eventually_inf — Mathlib

English

The eventual truth in the infimum of two filters is characterized by existence of witnesses in each filter and a compatibility condition on the intersection.

Русский

Истина относительно f ⊓ g выражается через существование множеств s ∈ f и t ∈ g такой, что ∀ x ∈ s ∩ t, p x.

LaTeX

$$$ (\forall^\infty x \in f \inf g,\ p x) \leftrightarrow \exists s \in f,\exists t \in g,\forall x \in s \cap t,\ p x $$$

Lean4

theorem eventually_inf {f g : Filter α} {p : α → Prop} : (∀ᶠ x in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x :=
  mem_inf_iff_superset

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