English
The class of concepts forms a lattice under the order by inclusion of extents, with join and meet given by explicit formulas.
Русский
Множество концептов образует решётку относительно включения экстентов, где объединение и пересечение задаются явными формулами.
LaTeX
$$$\mathrm{Lattice}(\mathrm{Concept}\,\alpha\,\beta\,r) \text{ with } c \lor d \text{ defined by } (c \lor d).extent = \operatorname{lowerPolar}_r(c.intent \cap d.intent),\ (c \lor d).intent = c.intent \cap d.intent\;\text{(и аналогично для ∧)}$$$
Lean4
instance instLatticeConcept : Lattice (Concept α β r) :=
{ Concept.instSemilatticeInfConcept with
sup := (· ⊔ ·)
le_sup_left := fun _ _ => intent_subset_intent_iff.1 inter_subset_left
le_sup_right := fun _ _ => intent_subset_intent_iff.1 inter_subset_right
sup_le := fun c d e => by
simp_rw [← intent_subset_intent_iff]
exact subset_inter }
