transEquiv — Mathlib

English

Postcompose a PartialEquiv with an Equiv and relate to trans: e.transEquiv e' = e.trans e'.toPartialEquiv.

Русский

Постсочетание частичной эквивалентности с эквивалентностью и связь через trans: e.transEquiv e' = e.trans e'.toPartialEquiv.

LaTeX

$$$e.transEquiv e' = e.trans e'.toPartialEquiv$$$

Lean4

/-- Postcompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior. -/
@[simps!]
def transEquiv (e : PartialEquiv α β) (f' : β ≃ γ) : PartialEquiv α γ :=
  (e.trans f'.toPartialEquiv).copy _ rfl _ rfl e.source (inter_univ _) (f'.symm ⁻¹' e.target) (univ_inter _)

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