le_ciInf_mul — Mathlib

English

For a group with right-monotone multiplication, if a ≤ g(i)·h for all i, then a ≤ (inf_i g(i))·h.

Русский

Пусть правополярное монотонное умножение. Если для всех i выполняется a ≤ g(i)·h, то a ≤ (inf_i g(i))·h.

LaTeX

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

Lean4

@[to_additive]
theorem le_ciInf_mul [MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h :=
  mul_inv_le_iff_le_mul.mp <| le_ciInf fun _ => mul_inv_le_iff_le_mul.mpr <| H _

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