tag_injective — Mathlib

English

For fixed n, ν ↦ tag(n,ν) is an injective map from ι → ℤ to ι → ℝ.

Русский

Для фиксированного n отображение ν ↦ tag(n,ν) из ι → ℤ в ι → ℝ инъективно.

LaTeX

$$Injective mapping: (ν ↦ tag(n,ν)) is injective.$$

Lean4

theorem tag_injective : Function.Injective (fun ν : ι → ℤ ↦ tag n ν) :=
  by
  refine fun _ _ h ↦ funext_iff.mpr fun i ↦ ?_
  have := congr_arg (fun x ↦ x i) h
  simp_rw [tag_apply, div_left_inj' (c := (n : ℝ)) (Nat.cast_ne_zero.mpr (NeZero.ne n)), add_left_inj,
    Int.cast_inj] at this
  exact this

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