α : Type u_1
β : Type ?u.92310
γ : Type ?u.92313
ι : Type ?u.92316
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
α : Type u_1
β : Type ?u.92310
γ : Type ?u.92313
ι : Type ?u.92316
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n} → b ≤ ⊥
simp [eq_univ_iff_forall]
no goals
α : Type u_1
β : Type ?u.92310
γ : Type ?u.92313
ι : Type ?u.92316
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
exact fun b hb => bot_unique <| hb _