exists_finset_of_mem_iSup — Mathlib

English

If m lies in the supremum of a family of submodules p i, then there exists a finite subset s such that m lies in the supremum of p i over i ∈ s.

Русский

Если m лежит в верхней грани i-ой совокупности p i, то существует конечное подмножество s такое, что m лежит в верхней грани p i для i ∈ s.

LaTeX

$$$\exists s: \mathrm{Finset}\ i,\; m \in \bigvee_{i \in s} p(i)$$$

Lean4

theorem exists_finset_of_mem_iSup {ι : Sort _} (p : ι → Submodule R M) {m : M} (hm : m ∈ ⨆ i, p i) :
    ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i :=
  by
  have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p
  simp only [Submodule.span_singleton_le_iff_mem] at this
  exact this hm

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