supClosure_mono

Mathlib.Order.SupClosed

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

English

The map s ↦ supClosure(s) is monotone: s ⊆ t implies supClosure(s) ⊆ supClosure(t).

Русский

Отображение s ↦ supClosure(s) монотонно: если s ⊆ t, то supClosure(s) ⊆ supClosure(t).

LaTeX

$$$s \\subseteq t \\Rightarrow \\operatorname{supClosure}(s) \\subseteq \\operatorname{supClosure}(t)$$$

Lean4

theorem supClosure_mono : Monotone (supClosure : Set α → Set α) :=
  supClosure.monotone

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

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

Разделы

Аффилиация

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