lowerPolar_empty

Mathlib.Order.Concept

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

English

For any r, lowerPolar r ∅ equals univ.

Русский

Для любого r, lowerPolar r пустого множества равно всему множеству.

LaTeX

$$$\lowerPolar\,r\, \emptyset = \mathrm{univ}$$$

Lean4

@[simp]
theorem lowerPolar_empty : lowerPolar r ∅ = univ :=
  upperPolar_empty _

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

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

Разделы

Аффилиация

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