isInternal_submodule_iff_iSupIndep_and_iSup_eq_top

English

Over a ring, IsInternal A is equivalent to iSupIndep A and iSup A = ⊤.

Русский

Для кольца IsInternal A эквивалентно iSupIndep A и iSup A = ⊤.

LaTeX

$$IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤$$

Lean4

/-- `iff` version of `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top`,
`DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
theorem isInternal_submodule_iff_iSupIndep_and_iSup_eq_top (A : ι → Submodule R M) :
    IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤ :=
  ⟨fun i ↦ ⟨i.submodule_iSupIndep, i.submodule_iSup_eq_top⟩, And.rec isInternal_submodule_of_iSupIndep_of_iSup_eq_top⟩

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