English
For elements a and b in a finite set s, the membership of a in s without b equals the conjunction of a ≠ b and a ∈ s.
Русский
Членство элемента a в множесте s без элемента b эквивалентно сочетанию a ≠ b и a ∈ s.
LaTeX
$$$a \\in s \\setminus \\{b\\} \\;\\;\\Longleftrightarrow\\;\\; (a \\neq b) \\land (a \\in s)$$$
Lean4
@[to_additive]
theorem prod_filter_of_pairwise_eq_one [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} (hn : n ∈ I)
(hf : (I : Set κ).Pairwise fun i j ↦ f i = f j → g (f i) = 1) : ∏ j ∈ I with f j = f n, g (f j) = g (f n) := by
classical
have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 :=
by
simp only [mem_erase, mem_filter] at hj
exact hf hj.2.1 hn hj.1 hj.2.2
rw [← mul_one (g (f n)), ← prod_eq_one h, ←
mul_prod_erase ({i ∈ I | f i = f n}) (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]
