exists_finset_of_mem_supr' — Mathlib

English

If x is in the supremum of the image of a family under a construction, there exists a finite index set whose join already contains x.

Русский

Если x принадлежит суперобъединению изображения семейства, существует конечное подмножество индексов, чьё объединение уже содержит x.

LaTeX

$$∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, f i$$

Lean4

theorem exists_finset_of_mem_supr' {ι : Type*} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ i, f i) :
    ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, F⟮(i.2 : E)⟯ :=
  by
  refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)
  exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)

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