subset_upperPolar_lowerPolar — Mathlib

English

Every subset t is contained in the upper polar of its lower polar: t ⊆ upperPolar r (lowerPolar r t).

Русский

Каждое подмножество t содержится в верхней полярной нижнего полярного множества: t ⊆ upperPolar r (lowerPolar r t).

LaTeX

$$$t \subseteq \upperPolar r (\lowerPolar r t)$$$

Lean4

theorem subset_upperPolar_lowerPolar (t : Set β) : t ⊆ upperPolar r (lowerPolar r t) :=
  subset_lowerPolar_upperPolar _ t

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