SubsetEq

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

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

Attributes Summary

known_left_sides
known_right_sides

Methods Summary

apply_transitivity(self, other, …)	Apply a transitivity rule to derive from this A subseteq B expression and something of the form B subseteq C, B subset C, or B=C to obtain A subset C or A subseteq C as appropriate.
conclude(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_as_folded(self, \*\*defaults_config)	Derive this folded version, A subseteq B, from the unfolded version, (forall_{x in A} x in B).
conclude_via_equality(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_equivalence(self, …)	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 SubsetEq statement is in the Boolean set.
derive_subset_nonmembership(self, element, …)	From A subset_eq B and element x not_in B, derive x not_in A.
derive_superset_membership(self, element, …)	From A subset_eq B and element x in A, derive x in B.
remake_constructor(self)	Method to call to reconstruct this Expression.
reversed_operator_str(format_type)	Reversing subset_eq gives superset_eq.
unfold(self[, elem_instance_var])	From A subset_eq B, derive and return (forall_{x in A} x in B).

Attributes Documentation

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

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

Methods Documentation

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

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

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

conclude(self, \*\*defaults_config)

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

conclude_as_folded(self, \*\*defaults_config)

Derive this folded version, A subseteq B, from the unfolded version, (forall_{x in A} x in B).

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

conclude_via_equality(self, \*\*defaults_config)

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

conclude_via_equivalence(self, \*\*defaults_config)

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 SubsetEq statement is in the Boolean set.

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

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

From A subset_eq B and element x not_in B, derive x not_in A.

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

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

From A subset_eq B and element 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 subset_eq gives superset_eq.

unfold(self, elem_instance_var=None, \*\*defaults_config)

From A subset_eq B, derive and return (forall_{x in A} x in B). x will be relabeled if an elem_instance_var is supplied.

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