map₂_iSup_left — Mathlib

English

Map₂ commutes with iSup on the left: map₂ f (iSup i s_i) t = iSup i map₂ f (s_i) t.

Русский

Map₂ коммутирует iSup слева: map₂ f (iSup_i s_i) t = iSup_i map₂ f (s_i) t.

LaTeX

$$map₂ f (iSup fun i => s i) t = iSup fun i => map₂ f (s i) t$$

Lean4

theorem map₂_iSup_left (f : M →ₗ[R] N →ₗ[R] P) (s : ι → Submodule R M) (t : Submodule R N) :
    map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t :=
  by
  suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

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