single_injective — Mathlib

English

For a fixed index i, the map single i : β(i) → Π₀ i, β(i) is injective. Distinct values placed at position i yield different total functions.

Русский

Для фиксированного индекса i отображение single i: β(i) → Π₀ i, β(i) являются инъекцией. Различные значения, помещаемые в позицию i, дают разные целевые функции.

LaTeX

$$$\operatorname{Injective}(\mathrm{single}_i: \beta(i) \to \Pi_0 i, \beta(i))$$$

Lean4

theorem single_injective {i} : Function.Injective (single i : β i → Π₀ i, β i) := fun _ _ H =>
  Pi.single_injective i <| DFunLike.coe_injective.eq_iff.mpr H

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