exists_sSupIndep_sSup_simples_eq_top

English

There exists a set s of submodules such that sSupIndep s holds, the supremum of s is top, and every member of s is simple.

Русский

Существует множество подмодулей s, которые независимы в смысле sSupIndep, их сомпределение достигает верха, и каждый элемент прост.

LaTeX

$$∃ s ⊆ Submodule R M, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m$$

Lean4

theorem exists_sSupIndep_sSup_simples_eq_top :
    ∃ s : Set (Submodule R M), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m :=
  by
  have := sSup_simples_eq_top R M
  simp_rw [isSimpleModule_iff_isAtom] at this ⊢
  exact exists_sSupIndep_of_sSup_atoms_eq_top this

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