trans_toPartialEquiv — Mathlib

English

Precompose an equivalence with a partial equivalence: the resulting object is the translation of the composed maps into a PartialEquiv.

Русский

Предсоставление эквивалентности частичным эквивалентом: полученный объект соответствует преобразованию составных отображений в PartialEquiv.

LaTeX

$$$(e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv$$$

Lean4

@[simp, mfld_simps]
theorem trans_toPartialEquiv : (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [PartialEquiv.trans_source, Equiv.toPartialEquiv])

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