copy_eq — Mathlib

English

Under the same hypotheses as the copy construction, the resulting copy equals the original, i.e., e.copy f hf g hg s hs t ht = e.

Русский

При тех же условиях копирования полученная копия равна исходному частичному эквивy, то есть e.copy f hf g hg s hs t ht = e.

LaTeX

$$$e.copy\ f\ hf\ g\ hg\ s\ hh\ t\ ht = e$$$

Lean4

theorem copy_eq (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α)
    (hs : e.source = s) (t : Set β) (ht : e.target = t) : e.copy f hf g hg s hs t ht = e :=
  by
  substs f g s t
  cases e
  rfl

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