English
Let e: α ≃ β be a bijection and s ⊆ β be a finite subset. Then e restricts to a bijection between e^{-1}(s) and s, with inverse given by e^{-1} restricted to s.
Русский
Пусть e: α ≃ β — биекция и s ⊆ β — конечное подмножество. Тогда e ограничивает отображение на биекции между e^{-1}(s) и s, с обратным отображением, задаваемым ограничением e^{-1} на s.
LaTeX
$$$e: \alpha \simeq \beta$ и $s \subseteq \beta$; тогда ограничение $e$ на $e^{-1}(s)$ даёт биекцию $e|_{e^{-1}(s)} : e^{-1}(s) \to s$ с обратной картой $e^{-1}|_s$.$$
Lean4
/-- Reindexing and then restricting to a `Finset` is the same as first restricting to the preimage
of this `Finset` and then reindexing. -/
theorem restrict_comp_piCongrLeft {π : β → Type*} (s : Finset β) (e : α ≃ β) :
s.restrict ∘ ⇑(e.piCongrLeft π) =
⇑((e.restrictPreimageFinset s).piCongrLeft (fun b : s ↦ (π b))) ∘ (s.preimage e e.injective.injOn).restrict :=
by
ext x b
simp only [comp_apply, restrict, Equiv.piCongrLeft_apply_eq_cast, Equiv.restrictPreimageFinset_symm_apply_coe]
