map_sInf_le

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#Monotone.map_sInf_le

English

Let f : α → β be monotone. Then f(sInf s) ≤ ⨅ a∈s, f(a).

Русский

Пусть f монотонна. Тогда f(sInf s) ≤ ⨅_{a∈s} f(a).

LaTeX

$$$f(\\\\,sInf\\\\ s) \\\\le \\\\iInf_{a\\\\in s} f(a)$$$

Lean4

theorem map_sInf_le [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : f (sInf s) ≤ ⨅ a ∈ s, f a :=
  hf.dual_left.map_sSup_le

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

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

Разделы

Аффилиация

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