iInf₂_le_of_le — Mathlib

English

If i, j are such that f(i)(j) ≤ a, then ⨅ (i) (j), f(i)(j) ≤ a.

Русский

Если найдутся $i$ и $j$, такие что $f(i)(j) \\le a$, то инфиму́мум по двум индексам не выше $a$.

LaTeX

$$$$\\text{If } f(i,j) \\le a, \\text{ then } \\inf_i \\inf_j f(i,j) \\le a.$$$$

Lean4

theorem iInf₂_le_of_le {f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) : ⨅ (i) (j), f i j ≤ a :=
  (iInf₂_le i j).trans h

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