mem_iSup_iff_exists_finset — Mathlib

English

Membership in the supremum is equivalent to existence of a finite subcollection witnessing membership.

Русский

Членство в объединении эквивалентно существованию конечной подвыборки, которая это членство подтверждает.

LaTeX

$$(m ∈ ⨆ i, p i) ↔ ∃ s : Finset, m ∈ ⨆ i ∈ s, p i$$

Lean4

/-- `Submodule.exists_finset_of_mem_iSup` as an `iff` -/
theorem mem_iSup_iff_exists_finset {ι : Sort _} {p : ι → Submodule R M} {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i :=
  ⟨Submodule.exists_finset_of_mem_iSup p, fun ⟨_, hs⟩ => iSup_mono (fun i => (iSup_const_le : _ ≤ p i)) hs⟩

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