iInf_sup_iInf_le — Mathlib

English

For two sequences f,g: ι → α, the infimum of the two pointwise supremums is bounded by the infimum of pairwise maxima: (⨅ i, f i) ⊔ (⨅ i, g i) ≤ ⨅ i, f i ⊔ g i.

Русский

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

LaTeX

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

Lean4

theorem iInf_sup_iInf_le (f g : ι → α) : (⨅ i, f i) ⊔ ⨅ i, g i ≤ ⨅ i, f i ⊔ g i :=
  @le_iSup_inf_iSup αᵒᵈ ι _ f g

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