omegaLimit_eq_iInter — Mathlib

English

For a fixed v ∈ f, the omega-limit equals the intersection over all u ∈ f of the closures of image2 ϕ (u ∩ v) s.

Русский

Для фиксированного v ∈ f ω‑лимит равен пересечению по всем u ∈ f замыкания образа image2 ϕ (u ∩ v) s.

LaTeX

$$$ \omega f ϕ s = \bigcap_{u \in f.sets} \overline{\operatorname{image2} ϕ (u \cap v) s}. $$$

Lean4

theorem omegaLimit_eq_iInter : ω f ϕ s = ⋂ u : ↥f.sets, closure (image2 ϕ u s) :=
  biInter_eq_iInter _ _

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