upperClosure_anti

Mathlib.Order.UpperLower.Closure

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

English

The upper closure operator is antitone: if s ≤ t then upperClosure t ≤ upperClosure s.

Русский

Оператор верхнего замыкания антитоничесок: если s ⊆ t, то верхнее замыкание t ⊆ верхнее замыкание s.

LaTeX

$$Antitone(upperClosure)$$

Lean4

theorem upperClosure_anti : Antitone (upperClosure : Set α → UpperSet α) :=
  gc_upperClosure_coe.monotone_l

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

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

Разделы

Аффилиация

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