ι : Sort ?u.109474
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α
ι : Sort ?u.109474
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
⊢ IsCompactlyGenerated α
rw [wellFounded_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
no goals
ι : Sort ?u.109474
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α
exact ⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩