iInf_le_iInf₂ — Mathlib

English

For κ: ι → Sort* and f: ι → α, the infimum over i is less than or equal to the infimum over i and j: ⨅ i, f i ≤ ⨅ (i) (_ : κ i), f i.

Русский

Для κ: ι → Sort и f: ι → α инфиму́мум по i не больше инфиму́мум по i и j: ⨅ i f(i) ≤ ⨅ (i) (_: κ i), f(i).

LaTeX

$$$$\\inf_i f(i) \\le \\inf_i \\inf_j f(i,j).$$$$

Lean4

theorem iInf_le_iInf₂ (κ : ι → Sort*) (f : ι → α) : ⨅ i, f i ≤ ⨅ (i) (_ : κ i), f i :=
  le_iInf₂ fun i _ => iInf_le f i

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