English
The composition of two subtype-congruence permutations corresponds to the subtype-congruence of the composed base permutations on each part.
Русский
Произведение двух перестановок, согласованных по подтипам, соответствует конгруенции подтипов от композиции базовых перестановок на каждой части.
LaTeX
$$$$(ep.subtypeCongr en).trans (ep'.subtypeCongr en') = Perm.subtypeCongr(ep.trans ep', en.trans en').$$$$
Lean4
@[simp]
theorem trans : (ep.subtypeCongr en).trans (ep'.subtypeCongr en') = Perm.subtypeCongr (ep.trans ep') (en.trans en') :=
by
ext x
by_cases h : p x
· have : p (ep ⟨x, h⟩) := Subtype.property _
simp [h, this]
· have : ¬p (en ⟨x, h⟩) := Subtype.property (en _)
simp [h, this]
