iSup_le_iSup_of_subset

Mathlib.Order.CompleteLattice.Basic

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

English

If s ⊆ t then ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x.

Русский

Если s ⊆ t, то ⨆x∈s f x ≤ ⨆x∈t f x.

LaTeX

$$$$ s \\subseteq t \\rightarrow \\bigvee_{x \\in s} f(x) \\leq \\bigvee_{x \\in t} f(x) $$$$

Lean4

theorem iSup_le_iSup_of_subset {f : β → α} {s t : Set β} : s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x :=
  biSup_mono

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

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

Разделы

Аффилиация

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