Infinite_Set_is_Equivalent_to_Proper_Subset
Provedinfinite-set-is-equivalent-to-proper-subsetinfinite-setsproofwikiset-equivalencesubsets
A set is infinite it is equivalent to one of its proper subsets.
Preamble
import Mathlib.Data.Fintype.Card import Mathlib.Data.Set.Basic
Formal statement
theorem Infinite_Set_is_Equivalent_to_Proper_Subset {S : Type _} : Infinite S ↔ ∃ (T : Set S) (f : S ≃ T), T ⊂ Set.univ := by sorrySource