NotSubsetEq

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

Bases: proveit.relation.relation.Relation

Methods Summary

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 nsupset B, from the unfolded version, not(A supset B).
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this NotSubsetEq statement is in the Boolean set.
remake_constructor(self)	Method to call to reconstruct this Expression.
reversed_operator_str(format_type)	Reversing not_subset_eq gives not_superset_eq.
side_effects(self, judgment)	Yield methods to attempt as side-effects when this expression is proven as a judgment.
unfold(self, \*\*defaults_config)	From A nsubseteq B, derive and return not(supseteq(A, B)).

Methods Documentation

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 nsupset B, from the unfolded version, not(A supset B).

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

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 not_subset_eq gives not_superset_eq.

side_effects(self, judgment)

Yield methods to attempt as side-effects when this expression is proven as a judgment. These should each accept an ‘assumptions’ parameter. These should be obvious and useful consequences, trivial and limited. There is no need to call this manually; it is called automatically when the corresponding Judgment is created. It also may be desirable to store the judgment for future automation.

unfold(self, \*\*defaults_config)

From A nsubseteq B, derive and return not(supseteq(A, B)).

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