comap_iSup — Mathlib

English

Pullback along m commutes with arbitrary suprema: comap m (iSup f) = ⨆ i, comap m (f i).

Русский

Обратное изображение вдоль m commute с произвольной верхней суммой: comap m (iSup f) = ⨆ i, comap m (f i).

LaTeX

$$$ \\operatorname{comap}_m\\bigl( \\bigvee_i f(i) \\bigr) = \\bigvee_i \\operatorname{comap}_m(f(i)) $$$

Lean4

theorem comap_iSup {ι} {f : ι → Filter β} {m : α → β} : comap m (iSup f) = ⨆ i, comap m (f i) :=
  (gc_comap_kernMap m).l_iSup

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