map_coprod_prod — Mathlib

English

The map induced by coproducing f and g on p and q equals the coproduct-map of the images: map (coprod f g) (p.prod q) = map f p ⊔ map g q.

Русский

Отображение, индуцируемое копродуцированием f и g на p и q, равно копроизведению образов: map (coprod f g) (p.prod q) = map f p ⊔ map g q.

LaTeX

$$$ \\text{map}(\\text{coprod } f g) (p. prod q) = \\text{map} f p \\; \\sqcup \\; \\text{map} g q $$$

Lean4

theorem map_coprod_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M) (q : Submodule R M₂) :
    map (coprod f g) (p.prod q) = map f p ⊔ map g q :=
  coprod_map_prod f g p q

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