instCompleteLattice

Mathlib.Order.CompleteLattice.Basic

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

Lean4

instance instCompleteLattice : CompleteLattice Prop
    where
  __ := «Prop».instBoundedOrder
  __ := «Prop».instDistribLattice
  sSup s := ∃ a ∈ s, a
  le_sSup _ a h p := ⟨a, h, p⟩
  sSup_le _ _ h := fun ⟨b, h', p⟩ => h b h' p
  sInf s := ∀ a, a ∈ s → a
  sInf_le _ a h p := p a h
  le_sInf _ _ h p b hb := h b hb p

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

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

Разделы

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

Аффилиация

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