English
Convert an Equiv to a PartialEquiv by restricting its domain and codomain via an image equality.
Русский
Преобразовать эквивалент к частичному эквиваленту, ограничив его область определения и кодовую область по равенству образов.
LaTeX
$$$\{ x : \mathrm{Option} \alpha \; //\; x.isSome \} \cong \alpha$$$
Lean4
/-- Interpret an `Equiv` as a `PartialEquiv` by restricting it to `s` in the domain
and to `t` in the codomain. -/
@[simps -fullyApplied]
def _root_.Equiv.toPartialEquivOfImageEq (e : α ≃ β) (s : Set α) (t : Set β) (h : e '' s = t) : PartialEquiv α β
where
toFun := e
invFun := e.symm
source := s
target := t
map_source' _ hx := h ▸ mem_image_of_mem _ hx
map_target' x
hx := by
subst t
rcases hx with ⟨x, hx, rfl⟩
rwa [e.symm_apply_apply]
left_inv' x _ := e.symm_apply_apply x
right_inv' x _ := e.apply_symm_apply x
