iInf_le_iInf_of_subset

Mathlib.Order.CompleteLattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_le_iInf_of_subset {f : β → α} {s t : Set β} : s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x :=
  biInf_mono

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

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

Разделы

Аффилиация

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