MathAction #279 Equality fails for Set Any

Topics

FrontPage
- IssueTracker
  - #279 Equality fails for Set Any <-- You are here.

Equality of sets demands:

$x \in X \iff x \in Y \implies X=Y$

This axiom fails for the domain Set Any. For example:

fricas

(1) -> X:Set Any

Type: Void

fricas

Y:Set Any

Type: Void

fricas

X:=["x"]

$\label{eq1}\left\{ \verb#"x"# \right\}$

(1)

Type: Set(Any)

fricas

Y:=["x"]

$\label{eq2}\left\{ \verb#"x"# \right\}$

(2)

Type: Set(Any)

fricas

(X=Y)::Boolean

$\label{eq3} \mbox{\rm true}$

(3)

Type: Boolean

and

fricas

X:=[1.0]

$\label{eq4}\left\{{1.0}\right\}$

(4)

Type: Set(Any)

fricas

Y:=[1.0]

$\label{eq5}\left\{{1.0}\right\}$

(5)

Type: Set(Any)

fricas

(X=Y)::Boolean

$\label{eq6} \mbox{\rm true}$

(6)

Type: Boolean

But notice that the following cases work:

fricas

X:=[1]

$\label{eq7}\left\{ 1 \right\}$

(7)

Type: Set(Any)

fricas

Y:=[1]

$\label{eq8}\left\{ 1 \right\}$

(8)

Type: Set(Any)

fricas

(X=Y)::Boolean

$\label{eq9} \mbox{\rm true}$

(9)

Type: Boolean

fricas

Z:Set Union(String,Integer,Float)

Type: Void

fricas

W:Set Union(String,Integer,Float)

Type: Void

fricas

Z:=["x"]

$\label{eq10}\left\{ \verb#"x"# \right\}$

(10)

Type: Set(Union(String,Integer,Float))

fricas

W:=["x"]

$\label{eq11}\left\{ \verb#"x"# \right\}$

(11)

Type: Set(Union(String,Integer,Float))

fricas

(Z=W)::Boolean

$\label{eq12} \mbox{\rm true}$

(12)

Type: Boolean

... --kratt6, Fri, 28 Dec 2007 14:20:21 -0800 reply

Category: Axiom Mathematics => Axiom Library

... --test1, Wed, 23 Apr 2014 18:54:02 +0000 reply

Status: open => closed

Subject: (replying) Be Bold !!

	( 15 subscribers )