one_lt_prod_iff_of_one_le — Mathlib

English

For f: ι → M with 1 ≤ f, we have 1 < ∏ i f(i) iff 1 < f (in the pointwise order).

Русский

Для f: ι → M с 1 ≤ f выполняется 1 < ∏ i f(i) тогда и только тогда, когда 1 < f (в точечном порядке).

LaTeX

$$$1 \le f \Rightarrow 1 < \prod_i f(i) \iff 1 < f$$$

Lean4

@[to_additive sum_pos_iff_of_nonneg]
theorem one_lt_prod_iff_of_one_le (hf : 1 ≤ f) : 1 < ∏ i, f i ↔ 1 < f := by
  obtain rfl | hf := hf.eq_or_lt <;> simp [*, one_lt_prod]

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