replaceEquiv_eq_self — Mathlib

English

If e' equals the underlying partial equivalence of e, then replacing with e' yields e itself.

Русский

Если e' совпадает с базовой частичной эквивалентностью e, то замена даёт сам e.

LaTeX

$$$\forall e: OpenPartialHomeomorph\,X\,Y, \forall e': PartialEquiv\,X\,Y, \forall h: e.toPartialEquiv = e',\ e.replaceEquiv\,e'\,h = e.$$$

Lean4

theorem replaceEquiv_eq_self (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e') : e.replaceEquiv e' h = e :=
  by
  cases e
  subst e'
  rfl

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