map₂_sup_right — Mathlib

English

Map₂ commutes with suprema on the left: map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t.

Русский

Map₂ коммутирует взятие верхнего предела слева: map₂ f (⨆ i, s_i) t = ⨆ i, map₂ f (s_i) t.

LaTeX

$$map₂ f (\\u222e i, s i) t = \\u222e i, map₂ f (s i) t$$

Lean4

theorem map₂_sup_right (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q₁ q₂ : Submodule R N) :
    map₂ f p (q₁ ⊔ q₂) = map₂ f p q₁ ⊔ map₂ f p q₂ :=
  le_antisymm
    (map₂_le.2 fun _m hm _np hnp =>
      let ⟨_n, hn, _p, hp, hnp⟩ := mem_sup.1 hnp
      mem_sup.2 ⟨_, apply_mem_map₂ _ hm hn, _, apply_mem_map₂ _ hm hp, hnp ▸ (map_add _ _ _).symm⟩)
    (sup_le (map₂_le_map₂_right le_sup_left) (map₂_le_map₂_right le_sup_right))

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