lowerPolar_upperPolar_lowerPolar — Mathlib

English

Applying upper polar to a lower polar and then back yields the original lower polar: lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t.

Русский

Применение верхней полярной к нижней полярной и затем возврат даёт исходную нижнюю полярную: lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t.

LaTeX

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

Lean4

@[simp]
theorem lowerPolar_upperPolar_lowerPolar (t : Set β) : lowerPolar r (upperPolar r <| lowerPolar r t) = lowerPolar r t :=
  upperPolar_lowerPolar_upperPolar _ t

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