intent_sSup — Mathlib

English

For any set S of concepts, the intent of the supremum of S equals the intersection of the intents of all concepts in S.

Русский

Для любого множества концептов S intent (sSup S) равен пересечению intents всех концептов из S.

LaTeX

$$$$ \operatorname{intent}\bigl(\operatorname{sSup} S\bigr) = \bigcap_{c \in S} \operatorname{intent}(c). $$$$

Lean4

@[simp]
theorem intent_sSup (S : Set (Concept α β r)) : (sSup S).intent = ⋂ c ∈ S, intent c :=
  rfl

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