Demonstrations for the theory of proveit.logic.sets.cardinality

import proveit
from proveit.logic import Forall, Exists, Implies, Equals, NotEquals, Card, Set, Distinct, InSet
from proveit.numbers import greater_eq, num, four
from proveit import a, b, n, A, B, C, D, N, S
from proveit.numbers import NaturalPos
%begin demonstrations

enum_set_card

#Equals(Card(Set(x_iter1l)), Len(x_iter1l)).prove([Distinct(x_iter1l)])

from proveit.logic.sets.cardinality import distinct_subset_existence
distinct_subset_existence

 ⊢  

distinct_subset_existence.instantiate(assumptions=[InSet(n, NaturalPos)])

 ⊢  

distinct_subset_existence

#Card(S).distinct_subset_existence(elems = [A,B,C,D], assumptions=[Equals(Len([A,B,C,D]), N), greater_eq(Card(S), N),  InSet(l, NaturalPos), greater_eq(Len(S),four)])

distinct_pair_existence

#Card(S).distinct_subset_existence(elems = [A,B], assumptions=[greater_eq(Card(S), num(2)), InSet(l, NaturalPos)])

%end demonstrations