sup — Mathlib

English

Join of two semisimple submodules is semisimple.

Русский

Сумма двух полупрямых подмодулей полупрямой.

LaTeX

$$IsSemisimpleModule R ↥(p ⊔ q)$$

Lean4

theorem sup {p q : Submodule R M} (_ : IsSemisimpleModule R p) (_ : IsSemisimpleModule R q) :
    IsSemisimpleModule R ↥(p ⊔ q) := by
  let f : Bool → Submodule R M := Bool.rec q p
  rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
  exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule (by rintro (_ | _) _ <;> assumption)

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