le_iSup_inf_iSup — Mathlib

English

For two functions f,g: ι → α, the join of their pointwise infima is bounded by the infimum of the pointwise maxima: (⨆ i, f i) ∨ (⨆ i, g i) ≤ ⨅ i, (f i) ∨ (g i).

Русский

Для функций f,g: ι → α, объединение по значению от f и g оценивается сверху как максимум, а снизу как минимум: (⨆ i, f i) ∨ (⨆ i, g i) ≤ ⨅ i, (f i) ∨ (g i).

LaTeX

$$$\bigl(\bigvee_i f_i\bigr) \lor\bigl(\bigvee_i g_i\bigr) \le \bigwedge_i (f_i \lor g_i)$$$

Lean4

theorem le_iSup_inf_iSup (f g : ι → α) : ⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i :=
  le_inf (iSup_mono fun _ => inf_le_left) (iSup_mono fun _ => inf_le_right)

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