comap_sSup — Mathlib

English

Pullback along m distributes over supremum of a set of filters: comap m (sSup s) = ⨆ f ∈ s, comap m f.

Русский

Обратное изображение вдоль m распределяет над объединением множества фильтров: comap m (sSup s) = ⨆ f ∈ s, comap m f.

LaTeX

$$$ \\operatorname{comap}_m( \\mathrm{sSup}(s) ) = \\bigsqcup_{f \\in s} \\operatorname{comap}_m f $$$

Lean4

theorem comap_sSup {s : Set (Filter β)} {m : α → β} : comap m (sSup s) = ⨆ f ∈ s, comap m f := by
  simp only [sSup_eq_iSup, comap_iSup]

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