lowerPolar_anti

Mathlib.Order.Concept

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

English

The operation lowerPolar r is antitone with respect to set inclusion: if s ⊆ t, then lowerPolar r t ⊆ lowerPolar r s.

Русский

Функция lowerPolar r антимонотонна по включению: если s ⊆ t, то lowerPolar r t ⊆ lowerPolar r s.

LaTeX

$$$s \subseteq t \Rightarrow \lowerPolar r t \subseteq \lowerPolar r s$$$

Lean4

theorem lowerPolar_anti : Antitone (lowerPolar r) :=
  upperPolar_anti _

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

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

Разделы

Аффилиация

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