English
The complete lattice structure on the collection of structure groupoids is defined by infimum, supremum, and related lattice operations.
Русский
Обще собрание структуры-групоидов образует полную решётку под операциями inf, sup и прочими латтовыми операциями.
LaTeX
$$$\\text{CompleteLattice}(\\mathrm{StructureGroupoid}(H))$$$
Lean4
instance : CompleteLattice (StructureGroupoid H) :=
{ SetLike.instPartialOrder,
completeLatticeOfInf _
(by
exact fun s =>
⟨fun S Ss F hF => mem_iInter₂.mp hF S Ss, fun T Tl F fT =>
mem_iInter₂.mpr (fun i his => Tl his
fT)⟩) with
le := (· ≤ ·)
lt := (· < ·)
bot := instStructureGroupoidOrderBot.bot
bot_le := instStructureGroupoidOrderBot.bot_le
top := instStructureGroupoidOrderTop.top
le_top := instStructureGroupoidOrderTop.le_top
inf := (· ⊓ ·)
le_inf := fun _ _ _ h₁₂ h₁₃ _ hm ↦ ⟨h₁₂ hm, h₁₃ hm⟩
inf_le_left := fun _ _ _ ↦ And.left
inf_le_right := fun _ _ _ ↦ And.right }
