le_ciInf_mul_ciInf — Mathlib

English

Let a be below every product g(i)·h(j). Then a ≤ (inf_i g(i))·(inf_j h(j)).

Русский

Пусть a ≤ g(i)·h(j) для всех i,j. Тогда a ≤ (inf_i g(i))·(inf_j h(j)).

LaTeX

$$$\displaystyle \forall i,\forall j,\ a \le g(i)\cdot h(j) \quad\Rightarrow\quad a \le \Bigl(\inf_i g(i)\Bigr) \cdot \Bigl(\inf_j h(j)\Bigr)$$$

Lean4

@[to_additive]
theorem le_ciInf_mul_ciInf [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α}
    (H : ∀ i j, a ≤ g i * h j) : a ≤ iInf g * iInf h :=
  le_ciInf_mul fun _ => le_mul_ciInf <| H _

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