ZFC Class

Stream: mathlib4

[Yury G. Kudryashov]

I'm refactoring docs#Set to break the defeq with X → Prop. Should docs#Class become a Set or _ → Prop? The file uses one or another in different theorems/definitions.

[Yury G. Kudryashov]

CC: @Mario Carneiro

[Yury G. Kudryashov]

Also, should we rename it or move it to a namespace?

[Violeta Hernández]

We currently define it as Set ZFSet so we get the instances for free, but then we write it out as ZFSet -> Prop to match mathematical notation and avoid mixing up the two membership operations. I think this design was me four year ago's idea.

My current if controversial idea would be to get rid of Class altogether and just write down Set ZFSet directly. Or like, at least make it an abbrev.

[Edward van de Meent]

That still leaves the question of defeq abuse though...

[Violeta Hernández]

The former, is my answer to the original question.

[Edward van de Meent]

I agree that motivates the abuse, but doesn't suggest what way to avoid it

[Violeta Hernández]

That should be an easy fix, write x \in C instead of C x.

[Violeta Hernández]

This type is barely used so I imagine that refactor shouldn't take long

[Violeta Hernández]

I can probably do it if you're willing to give me a day or two