instInfSet

Mathlib.Order.BooleanSubalgebra

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

Lean4

/-- The inf of Boolean subalgebras is their intersection. -/
instance instInfSet : InfSet (BooleanSubalgebra α) where
  sInf
    S :=
    { carrier := ⋂ L ∈ S, L
      bot_mem' := mem_iInter₂.2 fun _ _ ↦ bot_mem
      compl_mem' := fun ha ↦ mem_iInter₂.2 fun L hL ↦ compl_mem <| mem_iInter₂.1 ha L hL
      supClosed' :=
        supClosed_sInter <| forall_mem_range.2 fun L ↦ supClosed_sInter <| forall_mem_range.2 fun _ ↦ L.supClosed
      infClosed' :=
        infClosed_sInter <| forall_mem_range.2 fun L ↦ infClosed_sInter <| forall_mem_range.2 fun _ ↦ L.infClosed }

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

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

Разделы

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

Аффилиация

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