proposition: Lemma cantor_diag2 {X : Type} (U : Ensemble X) (f : X -> (Ensemble X)) : ~ surjective_ens f U (fun V : Ensemble X => Included V U).
proof: Proof. intros Hf. pose (g := (fun x : X => In U x /\ ~ In (f x) x) : Ensemble X). pose proof (Hf g) as [x [Hx Hxg]]. { intros x [Hx _]. apply Hx. } assert (f x x = g x). { rewrite Hxg. reflexivity. } unfold g in H. unfold In in H. destruct (classic (f x x)). - apply (Prop_contradiction_neq (f x x) (U x /\ ~ f x x)); tauto. - apply (Prop_contradiction_neq (U x /\ ~ f x x) (f x x)); try tauto. congruence. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)