le_mul_ciInf — Mathlib

English

If a is below every left-multiplication of g by h, i.e., a ≤ g·h(j) for all j, then a ≤ g·inf_j h(j).

Русский

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

LaTeX

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

Lean4

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

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