single_left_injective — Mathlib

English

If each b i ≠ 0, then the map i ↦ single i (b i) is injective.

Русский

Если каждый b i ≠ 0, то отображение i ↦ single i (b i) инъективно.

LaTeX

$$$\left(\forall i, b_i \neq 0\right) \Rightarrow \mathrm{Injective}(\lambda i. \mathrm{single}\ i (b_i))$$$

Lean4

/-- `DFinsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
`DFinsupp.single_injective` -/
theorem single_left_injective {b : ∀ i : ι, β i} (h : ∀ i, b i ≠ 0) :
    Function.Injective (fun i => single i (b i) : ι → Π₀ i, β i) := fun _ _ H =>
  (((single_eq_single_iff _ _ _ _).mp H).resolve_right fun hb => h _ hb.1).left

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