upperPolar — Mathlib

English

The upper polar with respect to swap r is equal to the lower polar with respect to r.

Русский

Верхняя полярная часть по отношению к swap r равна нижней полярной части по отношению к r.

LaTeX

$$$\upperPolar(\mathrm{swap}\,r)\,t = \lowerPolar\,r\,t$$$

Lean4

/-- The upper polar of `s : Set α` along a relation `r : α → β → Prop` is the set of all elements
which `r` relates to all elements of `s`. -/
def upperPolar (s : Set α) : Set β :=
  {b | ∀ ⦃a⦄, a ∈ s → r a b}

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