comap_sup — Mathlib

English

Supremum is preserved by comap: comap m (g1 ⊔ g2) = comap m g1 ⊔ comap m g2.

Русский

Супремум сохраняется под comap: comap m (g1 ⊔ g2) = comap m g1 ⊔ comap m g2.

LaTeX

$$$ \\operatorname{comap}_m( g_1 \\sqcup g_2 ) = \\operatorname{comap}_m g_1 \\sqcup \\operatorname{comap}_m g_2 $$$

Lean4

theorem comap_sup : comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂ := by
  rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]

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