infClosure_mono

Mathlib.Order.SupClosed

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

English

infClosure is monotone: s ⊆ t implies infClosure(s) ⊆ infClosure(t).

Русский

infClosure монотонно: если s ⊆ t, то infClosure(s) ⊆ infClosure(t).

LaTeX

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

Lean4

theorem infClosure_mono : Monotone (infClosure : Set α → Set α) :=
  infClosure.monotone

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

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

Разделы

Аффилиация

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