uniqueCongr — Mathlib

English

If α is equivalent to β, then Unique α is equivalent to Unique β.

Русский

Если α эквивалентно β, то Unique α эквивалентно Unique β.

LaTeX

$$$$ (e : α \\simeq β) \\Rightarrow (Unique \\ α) \\simeq (Unique \\ β). $$$$

Lean4

/-- If `α` is equivalent to `β`, then `Unique α` is equivalent to `Unique β`. -/
def uniqueCongr (e : α ≃ β) : Unique α ≃ Unique β
    where
  toFun h := @Equiv.unique _ _ h e.symm
  invFun h := @Equiv.unique _ _ h e
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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