comap_sup — Mathlib

English

Pullback distributes over sup: the comap of a supremum equals the supremum of comaps.

Русский

Обратное отображение распределяется по объединению: comap g над m1 ⊔ m2 равно comap g над m1 и над m2, объединённое.

LaTeX

$$$$ (m_{1} \;\sqcup\; m_{2}).\mathrm{comap}\, g = m_{1}.\mathrm{comap}\, g \;\sqcup\; m_{2}.\mathrm{comap}\, g $$$$

Lean4

@[simp]
theorem comap_sup : (m₁ ⊔ m₂).comap g = m₁.comap g ⊔ m₂.comap g :=
  (gc_comap_map g).l_sup

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