English
Given a bijection e: α ↔ β, there is a corresponding equivalence between Finset α and Finset β that maps each Finset to its image under e.
Русский
Дана биекция e: α ≃ β, существует соответствующее эквививалентное отображение между Finset α и Finset β, переводя каждое Finset в образ под e.
LaTeX
$$$\\text{If } e: α \\simeq β, \\; e.\\mathrm{finsetCongr}: \\mathrm{Finset}(α) \\simeq \\mathrm{Finset}(β)$, defined by $s \\mapsto s.map(e.toEmbedding)$ and $s \\mapsto s.map(e.symm.toEmbedding)$.$$
Lean4
/-- Given an equivalence `α` to `β`, produce an equivalence between `Finset α` and `Finset β`. -/
protected def finsetCongr (e : α ≃ β) : Finset α ≃ Finset β
where
toFun s := s.map e.toEmbedding
invFun s := s.map e.symm.toEmbedding
left_inv s := by simp [Finset.map_map]
right_inv s := by simp [Finset.map_map]
