CompleteLattice (WithBot α)

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

variable (α : Type*)

theorem WithBot.sInf_empty [CompleteLattice α] :
    (sInf ∅ : WithBot α) = ⊤ := by
  rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]

noncomputable instance [CompleteLattice α] : CompleteLattice (WithBot α) where
  le_sSup s a has := le_csSup (OrderTop.bddAbove _) has
  sSup_le s a hsa := s.eq_empty_or_nonempty.elim (by rw [·, WithBot.sSup_empty]; exact bot_le)
    (csSup_le · hsa)
  sInf_le s a hsa := csInf_le (OrderBot.bddBelow _) hsa
  le_sInf s a has := s.eq_empty_or_nonempty.elim (by rw [·, WithBot.sInf_empty]; exact le_top)
    (le_csInf · has)

[Kenny Lau]

I came across this gap while reviewing #26287

[Eric Wieser]

I think I found the same gap while reviewing the same PR, but didn't actually try to prove it