instCompleteLattice

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.instCompleteLattice

Lean4

/-- BooleanSubalgebras of a lattice form a complete lattice. -/
instance instCompleteLattice : CompleteLattice (BooleanSubalgebra α)
    where
  bot := ⊥
  bot_le _S _a := by aesop
  top := ⊤
  le_top _S a _ha := mem_top
  inf := (· ⊓ ·)
  le_inf _L _M _N hM hN _a ha := ⟨hM ha, hN ha⟩
  inf_le_left _L _M _a := And.left
  inf_le_right _L _M _a := And.right
  __ := completeLatticeOfInf (BooleanSubalgebra α) fun _s ↦ IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf

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

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

Разделы

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

Аффилиация

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