Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I found a good constructive definition of proper subset and put it in there. Also I wrote improper subset.
Edit: also family of subsets; see below.
Given any way of expressing A as the intersection of a family of subsets of S, this family is inhabited.
However isn’t S = intersection({S})?
True, but also S = intersection({}). Therefore there is a way of expressing S as the intersection of a family of subsets which is not inhabited, so S is not proper.
Possibly your confusion is my fault, because I used the dangerous word ‘any’. I will change it to read ‘every’. That is, we are saying rather than .
You have to define “family of subsets of a set S”.
Yes, I assumed that the reader would know what that means. Perhaps we should link it and write family of subsets?
For the record, a family of foos is (in general) a function from some set (called the index set of the family) to the set of all foos. In the case of a family of subsets of , there is a trick that you can play with this definition if you want to be predicative and not assume the existence of the set of all subsets of . That’s worth recording, so I will write family of subsets.
you can’t just use the definition of family of sets
Right, that’s completely different. It is really not a good idea to think of a subset of as being a set; instead, a subset of has a set associated with it. See subset and set for discussion of these issues.
I have written family of subsets.
1 to 4 of 4