extent_sInf — Mathlib

English

Let S be a set of concepts. The extent of the infimum of S equals the intersection of the extents of all c ∈ S.

Русский

Область инфимума множества концептов S равна пересечению областей (extents) всех c ∈ S.

LaTeX

$$$$ \operatorname{extent}\bigl(\operatorname{sInf} S\bigr) = \bigcap_{c \in S} \operatorname{extent}(c). $$$$

Lean4

@[simp]
theorem extent_sInf (S : Set (Concept α β r)) : (sInf S).extent = ⋂ c ∈ S, extent c :=
  rfl

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