English
The top element of a complete sublattice L belongs to L.
Русский
Наивысший элемент подрешетки L принадлежит L.
LaTeX
$$$\top \in L$$$
Lean4
/-- To check that a subset is a complete sublattice, one does not need to check that it is closed
under binary `Sup` since this follows from the stronger `sSup` condition. Likewise for infima. -/
@[simps]
def mk' (carrier : Set α) (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier)
(sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier) : CompleteSublattice α
where
carrier := carrier
sSupClosed' := sSupClosed'
sInfClosed' := sInfClosed'
supClosed' := fun x hx y hy ↦
by
suffices x ⊔ y = sSup { x, y } by exact this ▸ sSupClosed' (fun z hz ↦ by aesop)
simp [sSup_singleton]
infClosed' := fun x hx y hy ↦
by
suffices x ⊓ y = sInf { x, y } by exact this ▸ sInfClosed' (fun z hz ↦ by aesop)
simp [sInf_singleton]
