forall_eventually_of_eventually_forall

English

If p x holds for all y in β eventually with respect to a filter f, then for every y, p x y holds eventually with respect to f.

Русский

Если для каждого y из β x выполняется p(x, y) часто в отношении фильтра f, то для каждого y ∈ β p(x, y) выполняется часто.

LaTeX

$$$ (\forall^\infty x \in f, \forall y,\ p x y) \rightarrow \forall y, \forall^\infty x \in f,\ p x y $$$

Lean4

theorem forall_eventually_of_eventually_forall {f : Filter α} {p : α → β → Prop} (h : ∀ᶠ x in f, ∀ y, p x y) :
    ∀ y, ∀ᶠ x in f, p x y := fun y => h.mono fun _ h => h y

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