instBoundedOrderConcept — Mathlib

English

The class of concepts forms a bounded ordered set with explicit top and bottom elements.

Русский

Класс концептов образует ограниченное упорядоченное множество с верхним и нижним пределами.

LaTeX

$$$\mathrm{BoundedOrder}(\mathrm{Concept}\,\alpha\,\beta\,r)$$$

Lean4

instance instBoundedOrderConcept : BoundedOrder (Concept α β r)
    where
  top := ⟨univ, upperPolar r univ, rfl, eq_univ_of_forall fun _ _ hb => hb trivial⟩
  le_top _ := subset_univ _
  bot := ⟨lowerPolar r univ, univ, eq_univ_of_forall fun _ _ ha => ha trivial, rfl⟩
  bot_le _ := intent_subset_intent_iff.1 <| subset_univ _

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