map_injOn — Mathlib

English

The map(d) is injective on the set { x : Fin n → ℕ | ∀ i, x(i) < d }. That is, if x1 and x2 lie in this box and map(d) x1 = map(d) x2, then x1 = x2.

Русский

Функция map(d) инъективна на множестве { x: Fin n → ℕ | ∀ i, x(i) < d }. То есть если x1 и x2 лежат в этой коробке и map(d) x1 = map(d) x2, то x1 = x2.

LaTeX

$$$ {x : Fin\\ n → ℕ \\mid ∀ i, x i < d}.InjOn (map(d)) $$$

Lean4

theorem map_injOn : {x : Fin n → ℕ | ∀ i, x i < d}.InjOn (map d) :=
  by
  intro x₁ hx₁ x₂ hx₂ h
  induction n with
  | zero => simp [eq_iff_true_of_subsingleton]
  | succ n ih =>
    ext i
    have x := (map_eq_iff hx₁ hx₂).1 h
    exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

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