English
If a Finset s of indices has each f x compact, then the Finset sup of f is compact.
Русский
Если для каждого x в Finset индексов f x компактно, то sup по s от f x компактно.
LaTeX
$$CompleteLattice.IsCompactElement.finsetSup {α} {β} [CompleteLattice α] (s : Finset β) (h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f)$$
Lean4
theorem isCompactElement_finsetSup {α β : Type*} [CompleteLattice α] {f : β → α} (s : Finset β)
(h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f) := by
classical
rw [isCompactElement_iff_le_of_directed_sSup_le]
intro d hemp hdir hsup
rw [← Function.id_comp f]
rw [← Finset.sup_image]
apply Finset.sup_le_of_le_directed d hemp hdir
rintro x hx
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
specialize h p hps
rw [isCompactElement_iff_le_of_directed_sSup_le] at h
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
simpa only [exists_prop]
