English
Given an equivalence e: α ≃ β and a finite set s ⊆ β, the restriction of e to the preimage s.preimage e is an equivalence with s, i.e., a bijection between e^{-1}(s) and s.
Русский
Пусть e: α ≃ β и конечное множество s ⊂ β; ограничение e на подмножество предобраза e образует биекцию между e^{-1}(s) и s.
LaTeX
$$(e : α ≃ β) (s : Finset β) : (s.preimage e e.injective.injOn) ≃ s$$
Lean4
/-- Given an equivalence `e : α ≃ β` and `s : Finset β`, restrict `e` to an equivalence
from `e ⁻¹' s` to `s`. -/
@[simps]
def restrictPreimageFinset (e : α ≃ β) (s : Finset β) : (s.preimage e e.injective.injOn) ≃ s
where
toFun a := ⟨e a, Finset.mem_preimage.1 a.2⟩
invFun b := ⟨e.symm b, by simp⟩
left_inv _ := by simp
right_inv _ := by simp
