sigmaCongrRightHom_injective — Mathlib

English

The monoid hom σ = sigmaCongrRightHom β is injective, i.e., if two families of permutations yield the same permutation on the total sigma-type, then the two families are identical.

Русский

Гомоморфизм sigmaCongrRightHom β инъективен: если две семейства перестановок дают одинаковую перестановку на суммарном типе Σ a β(a), то эти семейства совпадают.

LaTeX

$$$$ \text{Injective}\bigl(\sigma_{\beta}\bigr), \quad \forall f,g:\prod_{a\in\alpha}\mathrm{Perm}(\beta(a)),\ \sigma_{\beta}(f)=\sigma_{\beta}(g) \Rightarrow f=g. $$$$

Lean4

theorem sigmaCongrRightHom_injective {α : Type*} {β : α → Type*} : Function.Injective (sigmaCongrRightHom β) :=
  by
  intro x y h
  ext a b
  simpa using Equiv.congr_fun h ⟨a, b⟩

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