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

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import x, A, B, S
from proveit.logic import Boolean, EmptySet, Forall, Intersect, InSet, NotInSet
from proveit.logic import SetEquiv, SubsetEq, Union

%begin theorems

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

Nothing is in the empty set (everything is not in the empty set):

nothing_is_in_empty = Forall(x, NotInSet(x, EmptySet))

nothing_is_in_empty (conjecture without proof):

Identities Involving Unions, Intersections, and Equivalences

union_with_superset_is_superset = Forall(
        (A, S),
        SetEquiv(Union(A, S), S),
        conditions=[SubsetEq(A, S)])

union_with_superset_is_superset (conjecture without proof):

intersection_with_superset_is_set = Forall(
        (A, S),
        SetEquiv(Intersect(A, S), A),
        conditions=[SubsetEq(A, S)])

intersection_with_superset_is_set (conjecture without proof):

set_subset_eq_of_union_with_set = Forall(
    (A, B),
    SubsetEq(A, Union(A, B)),
    condition=Forall(x, InSet(InSet(x, B), Boolean)))

set_subset_eq_of_union_with_set (conjecture with conjecture-based proof):

intersection_is_subset_eq = Forall(
        (A, B),
        SubsetEq(Intersect(A, B), A),
    condition=Forall(x, InSet(InSet(x, B), Boolean)))

intersection_is_subset_eq (conjecture with conjecture-based proof):

intersection_subset_eq_union = Forall(
        (A, B),
        SubsetEq(Intersect(A, B), Union(A, B)))

intersection_subset_eq_union (conjecture with conjecture-based proof):

%end theorems

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