sInf_le_sInf

Mathlib.Order.CompleteLattice.Defs

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

English

If s ⊆ t, then sInf(t) ≤ sInf(s).

Русский

Если s ⊆ t, то sInf(t) ≤ sInf(s).

LaTeX

$$$s \subseteq t \Rightarrow sInf(t) \le sInf(s)$$$

Lean4

@[gcongr]
theorem sInf_le_sInf (h : s ⊆ t) : sInf t ≤ sInf s :=
  (isGLB_sInf s).mono (isGLB_sInf t) h

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

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

Разделы

Аффилиация

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