proposition: Lemma approximants_grow : forall A X:Ensemble U, ~ Finite U A -> forall n:nat, cardinal U X n -> Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A.
proof: Proof. intros A X H' n H'0; elim H'0; auto with sets. - intro H'1. cut (Inhabited U (Setminus U A (Empty_set U))). + intro H'2; elim H'2. intros x H'3. exists (Add U (Empty_set U) x); auto with sets. split. * apply card_add; auto with sets. * cut (In U A x). -- intro H'4; red; auto with sets. intros x0 H'5; elim H'5; auto with sets. intros x1 H'6; elim H'6; auto with sets. -- elim H'3; auto with sets. + apply make_new_approximant; auto with sets. - intros A0 n0 H'1 H'2 x H'3 H'5. lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets. intros x0 H'2; try assumption. elim H'2; intros H'7 H'8; try exact H'8; clear H'2. elim (make_new_approximant A x0); auto with sets. + intros x1 H'2; try assumption. exists (Add U x0 x1); auto with sets. split. * apply card_add; auto with sets. elim H'2; auto with sets. * red. intros x2 H'9; elim H'9; auto with sets. intros x3 H'10; elim H'10; auto with sets. elim H'2; auto with sets. + auto with sets. apply Defn_of_Approximant; auto with sets. apply cardinal_finite with (n := S n0); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image