lowerPolar — Mathlib

English

The lower polar with respect to swap r equals the upper polar with respect to r.

Русский

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

LaTeX

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

Lean4

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

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