English
Let S be a set of concepts in a context with relation r between α and β. Then the extent of the supremum of S equals the lower polar of r evaluated at the intersection of the intents of all concepts in S.
Русский
Пусть S—множество концептов в контексте с отношением r между α и β. Тогда область (extent) наибольшего концепта из S равна нижней полярной r на пересечении намерений всех концептов из S.
LaTeX
$$$$\operatorname{extent}\bigl(\operatorname{sSup} S\bigr) = \operatorname{lowerPolar}_r\left(\bigcap_{c \in S} \operatorname{intent}(c)\right). $$$$
Lean4
@[simp]
theorem extent_sSup (S : Set (Concept α β r)) : (sSup S).extent = lowerPolar r (⋂ c ∈ S, intent c) :=
rfl
