instCompleteLattice

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.instCompleteLattice

Lean4

instance : CompleteLattice (Subgroupoid C) :=
  {
    completeLatticeOfInf (Subgroupoid C)
      (by
        refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩ <;> simp only [mem_sInf]
        exacts [fun hp => hp S Ss, fun S Ss => Tl Ss
            fT]) with
    bot := ⊥
    bot_le := fun _ => empty_subset _
    top := ⊤
    le_top := fun _ => subset_univ _
    inf := (· ⊓ ·)
    le_inf := fun _ _ _ RS RT _ pR => ⟨RS pR, RT pR⟩
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru