intent_sInf — Mathlib

English

For any S, the intent of the infimum of S is the upper polar of r evaluated at the intersection of extents of all c ∈ S.

Русский

Для множества S намерение инфимума S равно верхней полярной polar_r на пересечение областей (extent) всех c ∈ S.

LaTeX

$$$$ \operatorname{intent}\bigl(\operatorname{sInf} S\bigr) = \operatorname{upperPolar}_r\left(\bigcap_{c \in S} \operatorname{extent}(c)\right). $$$$

Lean4

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

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