lowerClosure_mono

Mathlib.Order.UpperLower.Closure

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

English

The lower closure operator is monotone: if s ⊆ t then lowerClosure(s) ⊆ lowerClosure(t).

Русский

Оператор нижнего замыкания монотонен: если s ⊆ t, то lowerClosure(s) ⊆ lowerClosure(t).

LaTeX

$$Monotone(lowerClosure)$$

Lean4

theorem lowerClosure_mono : Monotone (lowerClosure : Set α → LowerSet α) :=
  gc_lowerClosure_coe.monotone_l

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

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

Разделы

Аффилиация

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