upperPolar_lowerPolar_upperPolar — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem upperPolar_lowerPolar_upperPolar (s : Set α) : upperPolar r (lowerPolar r <| upperPolar r s) = upperPolar r s :=
  (gc_upperPolar_lowerPolar r).l_u_l_eq_l _

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