map₂_iSup_right — Mathlib

English

Map₂ commutes with iSup on the right: map₂ f s (iSup i t_i) = iSup i map₂ f s (t_i).

Русский

Map₂ коммутирует iSup справа: map₂ f s (iSup_i t_i) = iSup_i map₂ f s (t_i).

LaTeX

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

Lean4

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

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