English
Let f : ι → F be a map and s a finite set. The Separable of ∏ i∈s (X − C(f(i))) is equivalent to a condition on f being injective on s.
Русский
Пусть f : ι → F, данные s конечны. Сепарабельность произведения ∏_{i∈s} (X − C(f(i))) эквивалентна условию инъективности f на s.
LaTeX
$$$ (\prod_{i\in s} (X - C(f_i))).Separable \iff \forall x\in s, \forall y\in s, f_x = f_y \Rightarrow x=y$$$
Lean4
theorem separable_prod_X_sub_C_iff' {ι : Sort _} {f : ι → F} {s : Finset ι} :
(∏ i ∈ s, (X - C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
⟨fun hfs _ hx _ hy hfxy => hfs.inj_of_prod_X_sub_C hx hy hfxy, fun H =>
by
rw [← prod_attach]
exact
separable_prod'
(fun x _hx y _hy hxy =>
@pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
(fun x y hxy => Subtype.eq <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
fun _ _ => separable_X_sub_C⟩
