omegaLimit_iUnion — Mathlib

English

If v ∈ f, then ω f ϕ s equals the intersection over u ∈ f of closure(image2 ϕ (u ∩ v) s).

Русский

При v ∈ f имеем: ω f ϕ s = ⋂ u ∈ f closure(image2 ϕ (u ∩ v) s).

LaTeX

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

Lean4

theorem omegaLimit_iUnion (p : ι → Set α) : ⋃ i, ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i) :=
  by
  rw [iUnion_subset_iff]
  exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)

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