exists_finset_of_mem_iSup — Mathlib

English

If x lies in the supremum over i of f_i, there exists a finite subset s of indices such that x lies in the supremum over i in s of f_i.

Русский

Если x лежит в iSup f_i, то существует конечное множество индексов s, для которых x лежит в ⨆ i∈s f_i.

LaTeX

$$∃ s : Finset ι, x ∈ ⨆ i ∈ s, f_i$$

Lean4

theorem exists_finset_of_mem_iSup {ι : Type*} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ i, f i) :
    ∃ s : Finset ι, x ∈ ⨆ i ∈ s, f i :=
  by
  have := (adjoin_simple_isCompactElement x).exists_finset_of_le_iSup (IntermediateField F E) f
  simp only [adjoin_simple_le_iff] at this
  exact this hx

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