Theorems (or conjectures) for the theory of proveit.logic.sets.cardinality

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Forall, Exists, Implies, Equals, NotEquals, Card, Set, Distinct
from proveit.numbers import greater_eq, num
from proveit import a, b, n, N, S
from proveit.core_expr_types import Len
from proveit.core_expr_types import x_1_to_n
from proveit.numbers import NaturalPos
%begin theorems

Defining theorems for theory 'proveit.logic.sets.cardinality'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

The cardinality of an enumerated set of unique elements is the number of these unique elements:

enum_set_card = Forall(n, Forall(x_1_to_n, Equals(Card(Set(x_1_to_n)), Len(x_1_to_n)), 
                               conditions=[Distinct(x_1_to_n)]),
                    domain=NaturalPos)

enum_set_card (conjecture without proof):

If there are two or more elements in a set, there exists a pair of elements in the set that are not the same:

distinct_subset_existence = Forall(n, Forall((S, N), 
                                           Exists(x_1_to_n, Distinct(x_1_to_n), domain=S,
                                                  conditions=[Equals(Len(x_1_to_n), N)]),
                                           conditions=[greater_eq(Card(S), N)]),
                                 domain=NaturalPos)

distinct_subset_existence (conjecture without proof):

distinct_pair_existence = Forall(S, Exists((a, b), NotEquals(a, b), domain=S),
                               conditions=[greater_eq(Card(S), num(2))])

distinct_pair_existence (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.logic.sets.cardinality