prod_eq_sup_map — Mathlib

English

The product p × q equals the supremum of the images via inl and inr: p.prod q = map inl p ⊔ map inr q.

Русский

Произведение p × q равно наибольшему изобразив через inl и inr: p.prod q = map inl p ⊔ map inr q.

LaTeX

$$$ p \\text{.prod } q = \\text{map}(\\text{inl})\, p \\; \\sqcup \\; \\text{map}(\\text{inr})\, q $$$

Lean4

theorem prod_eq_sup_map (p : Submodule R M) (q : Submodule R M₂) :
    p.prod q = p.map (LinearMap.inl R M M₂) ⊔ q.map (LinearMap.inr R M M₂) := by
  rw [← map_coprod_prod, coprod_inl_inr, map_id]

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