prod_erase_lt_of_one_lt — Mathlib

English

If the product over a finite set s is equal to 1, and all elements except possibly one are 1, then all elements are 1.

Русский

Если произведение по конечному множеству s равно 1, и все элементы, за исключением одного, равны 1, то все элементы равны 1.

LaTeX

$$$\\forall x \\in s,\\; x \\\\neq a \\Rightarrow f(x) = 1\\;\n\\Rightarrow\\n\\forall x \\in s,\\; f(x) = 1$$$

Lean4

@[to_additive]
theorem prod_erase_lt_of_one_lt {κ : Type*} [DecidableEq ι] [CommMonoid κ] [LT κ] [MulLeftStrictMono κ] {s : Finset ι}
    {d : ι} (hd : d ∈ s) {f : ι → κ} (hdf : 1 < f d) : ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m :=
  by
  conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]
  rw [Finset.prod_insert (Finset.notMem_erase d s)]
  exact lt_mul_of_one_lt_left' _ hdf

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