le_map_iInf

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#Antitone.le_map_iInf

English

If f is antitone, then ⨆ i f(s i) ≤ f(iInf s).

Русский

Если f антитоническая, тогда ⨆ i f(s i) ≤ f(iInf s).

LaTeX

$$[Antitone] f → ⨆ i, f(s i) ≤ f(iInf s)$$

Lean4

theorem le_map_iInf [CompleteLattice β] {f : α → β} (hf : Antitone f) : ⨆ i, f (s i) ≤ f (iInf s) :=
  hf.dual_left.le_map_iSup

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

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

Разделы

Аффилиация

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