mul_ciSup_le — Mathlib

English

In a Group with a monotone left-multiplication, if g(j)·h ≤ a for all j, then g·(sup_j h(j)) ≤ a.

Русский

В группе с монотонным умножением слева: если для всех j выполняется g·h(j) ≤ a, то g·(sup_j h(j)) ≤ a.

LaTeX

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

Lean4

@[to_additive]
theorem mul_ciSup_le [MulLeftMono α] {a : α} {g : α} {h : ι → α} (H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a :=
  le_mul_ciInf (α := αᵒᵈ) H

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