le_hasProd — Mathlib

English

If HasProd f a L holds and i is arbitrary with all other indices bounded below by 1, then f(i) ≤ a.

Русский

Если HasProd f a L выполняется и для i произвольны, а все остальные индексы удовлетворяют f(j) ≥ 1, тогда f(i) ≤ a.

LaTeX

$$$\\forall f, a:\\, HasProd f a L \\to \\forall i:\\, ι, (\\forall j:\\, ι, j \\neq i \\to 1 \\le f(j)) \\to f(i) \\le a$$$

Lean4

@[to_additive]
theorem le_hasProd [L.NeBot] [L.LeAtTop] (hf : HasProd f a L) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) : f i ≤ a :=
  calc
    f i = ∏ i ∈ { i }, f i := by rw [prod_singleton]
    _ ≤ a := prod_le_hasProd _ (by simpa) hf

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