map₂_sup_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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