ConditionSet, ImageSet: Implement formal Set comprehension

[rws]

In order to be able to express solution sets from SymPy's solveset a set comprehension constructor as equivalent to SymPy's imageset / ConditionSet is needed. As the arguments are symbolic the most natural way to do this would be a formal symbolic function named like set_of_all taking a term argument and a list argument containing element_of(...) function expressions.

This set would convert to a SymPy ​ImageSet or ​ConditionSet

Related: ImageManifoldSubset (#31653)

[rws]

Accepting lists requires the function being a GinacFunction.

[rws]

New commits:

​669ea22	24171: Formal set membership function
​34c9773	24171: make RealSet inherit from Set_generic
​af82717	24171: remove RealSet import; SR set coercion doctests
​592ce87	24171: Py3 fixes
​82b7c6f	Merge branch 'u/rws/formal_set_membership_function' of git://trac.sagemath.org/sage into t/24176/implement_formal_set_comprehension
​ae29895	24176: check set argument of element_of()
​9c77312	24176: Implement formal Set comprehension

[mkoeppe]

Rebased on top of rebased #24171

---

New commits:

​72565f2	24171: Formal set membership function
​71bbf38	24171: Formal set membership function
​6811a76	24171: make RealSet inherit from Set_generic
​0a66f78	24171: remove RealSet import; SR set coercion doctests
​e35349a	24171: Py3 fixes
​26ef67d	24176: check set argument of element_of()
​ec39309	24176: Implement formal Set comprehension

[git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. Last 10 new commits:

​51c8152	Merge branch 't/31877/refine_category_of_realset' into t/24171/set-membership-rebased
​5e623bb	RealSet.is_finite: Remove, inherited from category
​7d19916	Do not use QQ.completion(oo,oo) - not implemented
​9b4e224	24176: check set argument of element_of()
​5310e04	Function_elementof: Remove use of is_Set
​46d9795	24171: Formal set membership function
​6995d1e	24171: make RealSet inherit from Set_generic
​a41c5fc	24171: remove RealSet import; SR set coercion doctests
​2a9c49a	24171: Py3 fixes
​24789ba	24176: Implement formal Set comprehension

[mkoeppe]

Rebased on top of updated #24171, which cherry-picked 1 commit from here.

Not sure about the changes on this ticket marked 24171. They are either from a newer or older version of 24171.

[mkoeppe]

The fix to RealSet.__bool__ in 6995d1e/2a9c49a can go to #31941 (Make empty RealSet false).

Unclear to me whether 6995d1e (make RealSet inherit from Set_generic) should be done

[mkoeppe]

I think the approach on the current branch may be tied a bit too closely to SR functions.

I think it's better to first implement:

• ImageSubset (as an abstract subobject of the codomain) for arbitrary Maps -- this would be a generalization of ImageManifoldSubset (#31653). No relation to SR (but by relaxing the code from #24171 that only allows some sets to be coerced to SR, one would be able to coerce it to SR).

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

[mkoeppe]

Replying to mkoeppe:

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

more precisely... an element of CallableSymbolicExpression (see #32008 for making this safer)

[mkoeppe]

Replying to mkoeppe:

Replying to mkoeppe:

• ConditionSet (as an abstract subobject of a parent in the Sets category) - defined via the element constructor of the parent and an SR expression with truth value.

more precisely... an element of CallableSymbolicExpression (see #32008 for making this safer)

This is now implemented in #32089.

[mkoeppe]

ImageSet is essentially the same as the (deprecated?) sage.combinat.combinat.MapCombinatorialClass, except that we would not insist that the map is injective.

[mkoeppe]

Opened #32121 Replace MapCombinatorialClass

[mantepse]

@mkoeppe: since you put me into the CC list, would this include symbolic roots of polynomials, given by the minimal polynomial?

I am guessing (because I'm not an expert there) that these would really need a special treatment, because one can compute with them quite well.