From fields to sets

Stream: general

[Anthony Bordg]

Hello,

is there an easy way to get the underlying set of a (discrete) field ?
Thanks

[Simon Hudon]

If you have field α, set.univ α is the underlying set.

[Anthony Bordg]

If you have field α, set.univ α is the underlying set.

Great! Thank you Simon.

[Simon Hudon]

:+1:

[Simon Hudon]

What do you use it for? Typically, I don't see that set used much because the type does most of the work on its own

[Mario Carneiro]

I think maybe you just want α?

[Mario Carneiro]

It's not an "underlying set", it's an "underlying type"

[Mario Carneiro]

and there is no underlying about it because we define "a field on α" rather than just "a field", so α is the carrier

[Anthony Bordg]

What do you use it for? Typically, I don't see that set used much because the type does most of the work on its own

You're right, I realized that I don't need it. :+1: