toPartialEquiv — Mathlib

English

Associate an Equiv to a PartialEquiv by restricting to entire domain and codomain using surjectivity.

Русский

Связать эквивалентность с частичным эквивалентом через ограничение на всю область определения и область значения, используя сюръективность.

LaTeX

$$$\mathrm{Equiv.toPartialEquiv}\ e$$$

Lean4

/-- Associate a `PartialEquiv` to an `Equiv`. -/
@[simps! (attr := mfld_simps) -fullyApplied]
def _root_.Equiv.toPartialEquiv (e : α ≃ β) : PartialEquiv α β :=
  e.toPartialEquivOfImageEq univ univ <| by rw [image_univ, e.surjective.range_eq]

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