mk_injective — Mathlib

English

For a fixed finite set s, the map x ↦ mk s x is injective.

Русский

Для фиксированного множества s отображение x ↦ mk s x инъективно.

LaTeX

$$$\forall x,y,\ (\mathrm{mk}\ s\ x = \mathrm{mk}\ s\ y) \Rightarrow x = y$$$

Lean4

theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β _ _ s) :=
  by
  intro x y H
  ext i
  have h1 : (mk s x : ∀ i, β i) i = (mk s y : ∀ i, β i) i := by rw [H]
  obtain ⟨i, hi : i ∈ s⟩ := i
  dsimp only [mk_apply, Subtype.coe_mk] at h1
  simpa only [dif_pos hi] using h1

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