English
The inverse of the subtype-congruence permutation equals the subtype-congruence of the inverses on the positive and negative parts.
Русский
Обратный элемент перестановки, порождённой конгруенцией подтипа, равен конгруенции подтипа от обратных элементов на положительной и отрицательной частях.
LaTeX
$$$$(ep.subtypeCongr en)^{-1} = Perm.subtypeCongr(ep^{-1}, en^{-1}).$$$$
Lean4
@[simp]
theorem symm : (ep.subtypeCongr en).symm = Perm.subtypeCongr ep.symm en.symm :=
by
ext x
by_cases h : p x
· have : p (ep.symm ⟨x, h⟩) := Subtype.property _
simp [h, symm_apply_eq, this]
· have : ¬p (en.symm ⟨x, h⟩) := Subtype.property (en.symm _)
simp [h, symm_apply_eq, this]
