SetLike
instance for elements of CompleteSublattice (Set X)
#
This file provides lemmas for the SetLike
instance for elements of CompleteSublattice (Set X)
@[simp]
@[simp]
@[simp]
theorem
CompleteSublattice.not_mem_bot
{X : Type u_1}
{L : CompleteSublattice (Set X)}
{x : X}
:
x ∉ ⊥