no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.112728
γ : Type ?u.112731
ι : Sort ?u.112734
ι' : Sort ?u.112737
κ : ι → Sort ?u.112742
κ' : ι' → Sort ?u.112747
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ (⨅ (x : β) (_ : x ∈ ∅), f x) = ⊤
simp