English
If k is compact, then for any collection f: ι → α with k ≤ ⨆ i, f i there exists a finite subset t of ι such that k ≤ ⨆ i ∈ t, f i.
Русский
Если k компактен, то для любой функции f: ι → α с k ≤ верхняя граница ⨆ i, f i существует конечное подмножество t ⊆ ι такое, что k ≤ ⨆ i ∈ t, f i.
LaTeX
$$∀ {k : α} (hk : IsCompactElement k) {ι : Type*} (f : ι → α), k ≤ ⨆ i, f i → ∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i$$
Lean4
theorem exists_finset_of_le_iSup {k : α} (hk : IsCompactElement k) {ι : Type*} (f : ι → α) (h : k ≤ ⨆ i, f i) :
∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i := by
classical
let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
have h1 : DirectedOn (· ≤ ·) (Set.range g) :=
by
rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
exact
⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
iSup_le_iSup_of_subset Finset.subset_union_right⟩
have h2 : k ≤ sSup (Set.range g) :=
h.trans
(iSup_le fun i =>
le_sSup_of_le ⟨{ i }, rfl⟩ (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
(isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g) h1 h2
exact ⟨s, hs⟩
