prod_symm — Mathlib

English

The product of partial equivalences commutes with taking inverses: (e.prod e').symm = e.symm.prod e'.symm.

Русский

Произведение частичных эквивалентностей и взятие обратного коммутируют: (e.prod e').symm = e.symm.prod e'.symm.

LaTeX

$$$ (e.prod e').symm = e.symm.prod e'.symm $$$

Lean4

@[simp, mfld_simps]
theorem prod_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.prod e').symm = e.symm.prod e'.symm := by
  ext x <;> simp [prod_coe_symm]

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