upperPolar_anti

Mathlib.Order.Concept

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

English

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

Русский

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

LaTeX

$$$s \subseteq t \Rightarrow \upperPolar r t \subseteq \upperPolar r s$$$

Lean4

theorem upperPolar_anti : Antitone (upperPolar r) :=
  (gc_upperPolar_lowerPolar r).monotone_l

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

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

Разделы

Аффилиация

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