upperPolar_swap

Mathlib.Order.Concept

URI: https://scilib.ai/kg/mathlib#upperPolar_swap

English

For any t, upperPolar (swap r) t equals lowerPolar r t.

Русский

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

LaTeX

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

Lean4

theorem upperPolar_swap (t : Set β) : upperPolar (swap r) t = lowerPolar r t :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru