Ugly proof of Uncountable (Type u)

Changes

1 changed files (+16/-0)

• Uncountable.lean (new)
  • @@ -0,0 +1,16 @@
    + import Mathlib + + #synth Uncountable Cardinal + + example : Uncountable (Type u) := by + by_contra! h + obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp h + let g (t : Type u) := Cardinal.mk t + let T := g '' Set.range f + obtain ⟨k, hk⟩ : ∃ k, k ∉ T := by + by_contra + have : T.Countable := Set.countable_range f |>.image g + have : T = .univ := by grind + grind [Set.not_countable_univ] + obtain ⟨t, ht⟩ : ∃ t, g t = k := ⟨_, k.mk_out⟩ + exact hk <| ht ▸ Set.mem_image_of_mem g (hf t)