No_Bijection_between_Finite_Set_and_Proper_Subset
Provedno-bijection-between-finite-set-and-proper-subsetproofwikiset-theorysubsets
A finite set can not be in one-to-one correspondence with one of its proper subsets. That is, a finite set is not Dedekind-infinite.
Preamble
import Mathlib.Data.Fintype.Card import Mathlib.Data.Set.Basic
Formal statement
theorem No_Bijection_between_Finite_Set_and_Proper_Subset {S : Type _} [Fintype S] (T : Set S) (hT : T ⊂ Set.univ) : ¬ ∃ f : S → T, Function.Bijective f := by sorrySource