omegaLimit_eq_biInter_inter — Mathlib

English

A compact decomposition: ω f ϕ s equals the intersection over all u ∈ f of the closures of image2 ϕ (u ∩ v) s, for any v ∈ f, under suitable conditions.

Русский

Компактное разложение: ω f ϕ s является пересечением по u ∈ f замыкания image2 ϕ (u ∩ v) s для некоторого v ∈ f при соблюдении условий.

LaTeX

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

Lean4

theorem omegaLimit_eq_biInter_inter {v : Set τ} (hv : v ∈ f) : ω f ϕ s = ⋂ u ∈ f, closure (image2 ϕ (u ∩ v) s) :=
  Subset.antisymm (iInter₂_mono' fun u hu ↦ ⟨u ∩ v, inter_mem hu hv, Subset.rfl⟩)
    (iInter₂_mono fun _u _hu ↦ closure_mono <| image2_subset inter_subset_left Subset.rfl)

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