subtypePerm_mul — Mathlib

English

The induced subtype permutation respects multiplication: the product of two subtypePerms equals the subtypePerm of the product with a combined preservation predicate.

Русский

Упорядоченная подтиповая перестановка сохраняет умножение: произведение двух подтиповых перестановок равно подтиповой перестановке от произведения с объединённым условием сохранения.

LaTeX

$$$$(\mathrm{subtypePerm} f hf * \mathrm{subtypePerm} g hg) = (\mathrm{subtypePerm} (f g) (\lambda x, (hf x).trans (hg x))).$$$$

Lean4

@[simp]
theorem subtypePerm_mul (f g : Perm α) (hf hg) :
    (f.subtypePerm hf * g.subtypePerm hg : Perm { x // p x }) = (f * g).subtypePerm fun _ => (hf _).trans <| hg _ :=
  rfl

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