subtypeCongrHom_injective — Mathlib

English

The map subtypeCongrHom is injective: the construction sending a pair of permutations on the two subtypes to a permutation of α is uniquely determined by its effect on α.

Русский

Гомоморфизм subtypeCongrHom инъективен: отображение пары перестановок на подтипах в перестановку на α однозначно определяется по действию на α.

LaTeX

$$$$ \text{Injective}(\mathrm{subtypeCongrHom}_p). $$$$

Lean4

theorem subtypeCongrHom_injective (p : α → Prop) [DecidablePred p] : Function.Injective (subtypeCongrHom p) :=
  by
  rintro ⟨⟩ ⟨⟩ h
  rw [Prod.mk_inj]
  constructor <;> ext i <;> simpa using Equiv.congr_fun h i

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