map₂_sup_right — Mathlib

English

The map₂ operation distributes over the supremum on the right: map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂.

Русский

Операция map₂ распределяется над верхней суммой справа: map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂.

LaTeX

$$$ map_2 m f (g_1 \sqcup g_2) = map_2 m f g_1 \sqcup map_2 m f g_2 $$$

Lean4

theorem map₂_sup_right : map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂ := by
  simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]

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