injective_of_prod_X_sub_C — Mathlib

English

If the separability of the product ∏ i (X − C(f_i)) holds, then f is injective on the index set.

Русский

Если произведение ∏_{i} (X − C(f_i)) сепарабельно, то отображение i ↦ f_i по индексам является инъективным.

LaTeX

$$$ \operatorname{Separable}\left( \prod_{i} (X - C(f_i)) \right) \Rightarrow \operatorname{Injective}(f)$$$

Lean4

theorem injective_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} [Fintype ι] {f : ι → R}
    (hfs : (∏ i, (X - C (f i))).Separable) : Function.Injective f := fun _x _y hfxy =>
  hfs.inj_of_prod_X_sub_C (mem_univ _) (mem_univ _) hfxy

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