lowerPolar_swap

Mathlib.Order.Concept

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

English

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

Русский

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

LaTeX

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

Lean4

theorem lowerPolar_swap (s : Set α) : lowerPolar (swap r) s = upperPolar r s :=
  rfl

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

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

Разделы

Аффилиация

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