ProperSubset

class proveit.logic.ProperSubset(A, B, *, styles=None)

Bases: proveit.logic.sets.inclusion.inclusion_relation.InclusionRelation

Class to represent proper subset relation, such as A proper_subset B, to represent the claim that any element in set A is also in set B, while B also has at least one element not in set A. Example usage: ProperSubset(A, B). Intended to replace the equivalent but more ambiguously-named Subset class.

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

apply_transitivity(self, other, …)	Apply a transitivity rule to derive from this ProperSubset(A, B) expression and something of the form SubsetEq(B, C), ProperSubset(B, C), or B=C, to obtain ProperSubset(A, C) as appropriate.
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this ProperSubset expression is in the Boolean set.
derive_relaxed(self, \*\*defaults_config)	From ProperSubset(A, B), derive SubsetEq(A, B).
derive_superset_membership(self, element, …)	From A subset B and x in A, derive x in B.
remake_constructor(self)	Method to call to reconstruct this Expression.
reversed_operator_str(format_type)	Reversing proper_subset gives proper_superset.
unfold(self, \*\*defaults_config)	From A proper_subset B, derive and return (A subset_eq B) and (B set_not_equiv A)

Attributes Documentation

known_left_sides = {{0}: OrderedSet([|- {0} proper_subset Integer, |- {0} proper_subset IntegerNonPos, |- {0} proper_subset Natural, |- {0} proper_subset Rational, |- {0} proper_subset RationalNonNeg, |- {0} proper_subset RationalNonPos, |- {0} proper_subset Real, |- {0} proper_subset RealNonNeg, |- {0} proper_subset RealNonPos, |- {0} proper_subset Complex]), _b: OrderedSet([{_b proper_subset _a} |- _b proper_subset _a]), A: OrderedSet([{A proper_subset B} |- A proper_subset B]), NaturalPos: OrderedSet([|- NaturalPos proper_subset Natural, |- NaturalPos proper_subset Integer, |- NaturalPos proper_subset IntegerNonZero, |- NaturalPos proper_subset RationalPos, |- NaturalPos proper_subset Real, |- NaturalPos proper_subset RealPos, |- NaturalPos proper_subset RealNonNeg, |- NaturalPos proper_subset ComplexNonZero]), Natural: OrderedSet([|- Natural proper_subset Integer, |- Natural proper_subset Rational, |- Natural proper_subset RationalNonNeg, |- Natural proper_subset Real, |- Natural proper_subset RealNonNeg, |- Natural proper_subset Complex]), IntegerNonZero: OrderedSet([|- IntegerNonZero proper_subset Integer, |- IntegerNonZero proper_subset RationalNonZero, |- IntegerNonZero proper_subset RealNonZero, |- IntegerNonZero proper_subset ComplexNonZero]), IntegerNeg: OrderedSet([|- IntegerNeg proper_subset Integer, |- IntegerNeg proper_subset IntegerNonZero, |- IntegerNeg proper_subset IntegerNonPos, |- IntegerNeg proper_subset RationalNeg, |- IntegerNeg proper_subset RealNeg, |- IntegerNeg proper_subset ComplexNonZero]), IntegerNonPos: OrderedSet([|- IntegerNonPos proper_subset Integer, |- IntegerNonPos proper_subset RationalNonPos, |- IntegerNonPos proper_subset RealNonPos, |- IntegerNonPos proper_subset Complex]), Integer: OrderedSet([|- Integer proper_subset Rational, |- Integer proper_subset Real, |- Integer proper_subset Complex]), RationalNonZero: OrderedSet([|- RationalNonZero proper_subset Rational, |- RationalNonZero proper_subset RealNonZero, |- RationalNonZero proper_subset ComplexNonZero]), RationalPos: OrderedSet([|- RationalPos proper_subset Rational, |- RationalPos proper_subset RationalNonZero, |- RationalPos proper_subset RationalNonNeg, |- RationalPos proper_subset RealPos]), RationalNeg: OrderedSet([|- RationalNeg proper_subset Rational, |- RationalNeg proper_subset RationalNonZero, |- RationalNeg proper_subset RationalNonPos, |- RationalNeg proper_subset RealNeg]), RationalNonNeg: OrderedSet([|- RationalNonNeg proper_subset Rational, |- RationalNonNeg proper_subset RealNonNeg, |- RationalNonNeg proper_subset Complex]), RationalNonPos: OrderedSet([|- RationalNonPos proper_subset Rational, |- RationalNonPos proper_subset RealNonPos, |- RationalNonPos proper_subset Complex, |- RationalNonPos proper_subset ComplexNonZero]), Rational: OrderedSet([|- Rational proper_subset Real, |- Rational proper_subset Complex]), RealPos: OrderedSet([|- RealPos proper_subset Real, |- RealPos proper_subset RealNonZero, |- RealPos proper_subset RealNonNeg]), RealNeg: OrderedSet([|- RealNeg proper_subset Real, |- RealNeg proper_subset RealNonZero, |- RealNeg proper_subset RealNonPos]), RealNonNeg: OrderedSet([|- RealNonNeg proper_subset Real, |- RealNonNeg proper_subset Complex]), RealNonPos: OrderedSet([|- RealNonPos proper_subset Real, |- RealNonPos proper_subset Complex, |- RealNonPos proper_subset ComplexNonZero]), RealNonZero: OrderedSet([|- RealNonZero proper_subset Real, |- RealNonZero proper_subset ComplexNonZero]), Real: OrderedSet([|- Real proper_subset Complex]), ComplexNonZero: OrderedSet([|- ComplexNonZero proper_subset Complex]), _c: OrderedSet([{_c proper_subset _b} |- _c proper_subset _b])}

known_right_sides = {Integer: OrderedSet([|- {0} proper_subset Integer, |- Natural proper_subset Integer, |- NaturalPos proper_subset Integer, |- IntegerNonZero proper_subset Integer, |- IntegerNeg proper_subset Integer, |- IntegerNonPos proper_subset Integer]), _a: OrderedSet([{_b proper_subset _a} |- _b proper_subset _a]), B: OrderedSet([{A proper_subset B} |- A proper_subset B]), IntegerNonPos: OrderedSet([|- {0} proper_subset IntegerNonPos, |- IntegerNeg proper_subset IntegerNonPos]), Natural: OrderedSet([|- {0} proper_subset Natural, |- NaturalPos proper_subset Natural]), IntegerNonZero: OrderedSet([|- NaturalPos proper_subset IntegerNonZero, |- IntegerNeg proper_subset IntegerNonZero]), Rational: OrderedSet([|- {0} proper_subset Rational, |- Natural proper_subset Rational, |- Integer proper_subset Rational, |- RationalNonZero proper_subset Rational, |- RationalPos proper_subset Rational, |- RationalNeg proper_subset Rational, |- RationalNonNeg proper_subset Rational, |- RationalNonPos proper_subset Rational]), RationalNonNeg: OrderedSet([|- {0} proper_subset RationalNonNeg, |- Natural proper_subset RationalNonNeg, |- RationalPos proper_subset RationalNonNeg]), RationalNonPos: OrderedSet([|- {0} proper_subset RationalNonPos, |- IntegerNonPos proper_subset RationalNonPos, |- RationalNeg proper_subset RationalNonPos]), RationalNonZero: OrderedSet([|- IntegerNonZero proper_subset RationalNonZero, |- RationalPos proper_subset RationalNonZero, |- RationalNeg proper_subset RationalNonZero]), RationalPos: OrderedSet([|- NaturalPos proper_subset RationalPos]), RationalNeg: OrderedSet([|- IntegerNeg proper_subset RationalNeg]), Real: OrderedSet([|- {0} proper_subset Real, |- Integer proper_subset Real, |- Natural proper_subset Real, |- NaturalPos proper_subset Real, |- Rational proper_subset Real, |- RealPos proper_subset Real, |- RealNeg proper_subset Real, |- RealNonNeg proper_subset Real, |- RealNonPos proper_subset Real, |- RealNonZero proper_subset Real]), RealNonNeg: OrderedSet([|- {0} proper_subset RealNonNeg, |- Natural proper_subset RealNonNeg, |- NaturalPos proper_subset RealNonNeg, |- RationalNonNeg proper_subset RealNonNeg, |- RealPos proper_subset RealNonNeg]), RealNonPos: OrderedSet([|- {0} proper_subset RealNonPos, |- IntegerNonPos proper_subset RealNonPos, |- RationalNonPos proper_subset RealNonPos, |- RealNeg proper_subset RealNonPos]), RealPos: OrderedSet([|- NaturalPos proper_subset RealPos, |- RationalPos proper_subset RealPos]), RealNonZero: OrderedSet([|- IntegerNonZero proper_subset RealNonZero, |- RationalNonZero proper_subset RealNonZero, |- RealPos proper_subset RealNonZero, |- RealNeg proper_subset RealNonZero]), RealNeg: OrderedSet([|- IntegerNeg proper_subset RealNeg, |- RationalNeg proper_subset RealNeg]), Complex: OrderedSet([|- {0} proper_subset Complex, |- Natural proper_subset Complex, |- Integer proper_subset Complex, |- IntegerNonPos proper_subset Complex, |- Rational proper_subset Complex, |- RationalNonNeg proper_subset Complex, |- RationalNonPos proper_subset Complex, |- Real proper_subset Complex, |- RealNonNeg proper_subset Complex, |- RealNonPos proper_subset Complex, |- ComplexNonZero proper_subset Complex]), ComplexNonZero: OrderedSet([|- IntegerNeg proper_subset ComplexNonZero, |- NaturalPos proper_subset ComplexNonZero, |- IntegerNonZero proper_subset ComplexNonZero, |- RationalNonPos proper_subset ComplexNonZero, |- RationalNonZero proper_subset ComplexNonZero, |- RealNonPos proper_subset ComplexNonZero, |- RealNonZero proper_subset ComplexNonZero]), _b: OrderedSet([{_c proper_subset _b} |- _c proper_subset _b])}

Methods Documentation

apply_transitivity(self, other, \*\*defaults_config)

Apply a transitivity rule to derive from this ProperSubset(A, B) expression and something of the form SubsetEq(B, C), ProperSubset(B, C), or B=C, to obtain ProperSubset(A, C) as appropriate.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this ProperSubset expression is in the Boolean set.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_relaxed(self, \*\*defaults_config)

From ProperSubset(A, B), derive SubsetEq(A, B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_superset_membership(self, element, \*\*defaults_config)

From A subset B and x in A, derive x in B.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

remake_constructor(self)

Method to call to reconstruct this Expression. The default is the class name itself to use the __init__ method, but sometimes a different method is more appropriate for setting the proper style (e.g. the Frac method in proveit.numbers.division.divide which constructs a Div object with a different style). This constructor method must be in the same module as the class.

static reversed_operator_str(format_type)

Reversing proper_subset gives proper_superset.

unfold(self, \*\*defaults_config)

From A proper_subset B, derive and return (A subset_eq B) and (B set_not_equiv A)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.