Use `structure`or `class` as a `Prop`

Stream: new members

[Han Han]

Now I often encounter the following problem: I want to use a structure or class as a proposition. For example, I want to formalize that an AddMonoidHom is not a RingHom. One possible solution is to write ¬ (∃ f : R →+* R, f.toAddMonoidHom = g). However, this feels a bit weird to me. How should I generally handle cases where I want to use a structure or class as a proposition?

[Han Han]

If there is no general method, could someone please provide a typical example to help me gain some experience?

[Kevin Buzzard]

What you write doesn't seem to me like a weird way of expressing what you want.

[Aaron Liu]

Maybe you'll find some examples in Counterexamples

[Han Han]

I think the example seems weird because I constantly have to convert between f and g. I’m looking for a more convenient way to formalize this.

[Han Han]

Kevin Buzzard said:

What you write doesn't seem to me like a weird way of expressing what you want.

I think the example seems weird because I constantly have to convert between f and g. I’m looking for a more convenient way to formalize this.

[Han Han]

Aaron Liu said:

Maybe you'll find some examples in Counterexamples

Thanks for your advice. That is a good idea.

[Matt Diamond]

I think it's worth adding that "this structure/class can/can't exist" is often expressed using docs#Nonempty and docs#IsEmpty