English
A partial isomorphism between α and β yields a natural partial isomorphism between β and α, obtained by swapping the coordinates of its graph.
Русский
Частичный изоморфизм между α и β порождает естественный частичный изоморфизм между β и α, получаемый перестановкой координат графа отображения.
LaTeX
$$$\\\\mathrm{comm}(f) = \\\\{(b,a) \\\\mid (a,b) \\\\\\in \\\\mathrm{val}(f)\\\\}.$$$
Lean4
/-- A partial isomorphism between `α` and `β` is also a partial isomorphism between `β` and `α`. -/
protected def comm : PartialIso α β → PartialIso β α :=
Subtype.map (Finset.image (Equiv.prodComm _ _)) fun f hf p hp q hq ↦
Eq.symm <|
hf ((Equiv.prodComm α β).symm p)
(by
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hp
rwa [← Finset.mem_coe])
((Equiv.prodComm α β).symm q)
(by
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage] at hq
rwa [← Finset.mem_coe])
