hasProd_one_iff_of_one_le — Mathlib

English

If every i satisfies f(i) ≥ 1, then HasProd f 1 L holds if and only if f = 1.

Русский

Если для каждого i выполняется f(i) ≥ 1, то HasProd f 1 L эквивалентно f = 1.

LaTeX

$$$\\forall f:\\, ι \\to α, (\\forall i, 1 \\le f i) \\to (HasProd f 1 L) \\leftrightarrow (f = 1)$$$

Lean4

@[to_additive]
theorem hasProd_one_iff_of_one_le [L.LeAtTop] [L.NeBot] (hf : ∀ i, 1 ≤ f i) : HasProd f 1 L ↔ f = 1 :=
  by
  refine ⟨fun hf' ↦ ?_, ?_⟩
  · ext i
    exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)
  · rintro rfl
    exact hasProd_one

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