mapEquiv_trans — Mathlib

English

The mapEquiv respects composition of equivalences: mapEquiv(f.trans g) = (mapEquiv f).trans (mapEquiv g).

Русский

MapEquiv сохраняет композицию эквивалентностей: mapEquiv(f.trans g) = mapEquiv(f).trans (mapEquiv(g)).

LaTeX

$$$\\mathrm{mapEquiv}(f\\,\\mathrm{trans}\\ g) = (\\mathrm{mapEquiv} f)\\,\\mathrm{trans}\\ (\\mathrm{mapEquiv} g)$$$

Lean4

@[simp]
theorem mapEquiv_trans (f : R ≃⋆* S) (g : S ≃⋆* T) : mapEquiv (f.trans g) = (mapEquiv f).trans (mapEquiv g) :=
  rfl

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