ofSubtype_injective — Mathlib

English

The inclusion map of Permutation on the subtype into Perm α is injective.

Русский

Включение перестановок подтипа в перестановки α инъективно.

LaTeX

$$$ \\text{Injective}(\\mathrm{ofSubtype} : \\operatorname{Perm}(\\operatorname{Subtype} p) \\to \\operatorname{Perm}(\\alpha)) $$$

Lean4

theorem ofSubtype_injective : Function.Injective (ofSubtype : Perm (Subtype p) → Perm α) :=
  by
  intro x y h
  rw [Perm.ext_iff] at h ⊢
  intro a
  specialize h a
  rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

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