map₂_sup_left — Mathlib

English

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

Русский

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

LaTeX

$$$ map_2 m (f_1 \sqcup f_2) g = map_2 m f_1 g \sqcup map_2 m f_2 g $$$

Lean4

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

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