eventually_iSup — Mathlib

English

Eventual property distributes over indexed suprema of filters: eventual p x in iSup fs b is equivalent to for all b, eventual p x in fs b.

Русский

Свойство выполняется относительно iSup распределяется по индексированным верхним пределам фильтров.

LaTeX

$$$ (\forall^\infty x \in iSup\ b,\ p x) \leftrightarrow \forall b,\forall^\infty x \in fs b,\ p x $$$

Lean4

@[simp]
theorem eventually_iSup {p : α → Prop} {fs : ι → Filter α} : (∀ᶠ x in ⨆ b, fs b, p x) ↔ ∀ b, ∀ᶠ x in fs b, p x :=
  mem_iSup

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