Set_Equivalence_Less_One_Element
Provedequivalence-relationsproofwiki
Let S and T be equivalent sets, and let a ∈ S and b ∈ T. Then S \ {a} ~ T \ {b}.
Preamble
import Mathlib.Logic.Equiv.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Set_Equivalence_Less_One_Element {α : Type _} {S T : Set α} (h : ∃ f : S ≃ T, True) (a : S) (b : T) : ∃ f : ({x : α | x ∈ S ∧ x ≠ a.val} ≃ {x : α | x ∈ T ∧ x ≠ b.val}), True := by sorrySource