Zulip Chat Archive

Stream: new members

Topic: Set complement (superscript c) notation defined?

Kevin Sullivan (Nov 29 2023 at 00:24):

For Set.compl. Checking. Thank you.

Jireh Loreaux (Nov 29 2023 at 01:36):

What's your question?

Kevin Sullivan (Nov 29 2023 at 01:37):

Jireh Loreaux said:

What's your question?

Is set complement (superscript c) notation provided by mathlib in Lean4?

Jeremy Tan (Nov 29 2023 at 01:37):

Yes, if you pull in the right import

Kevin Sullivan (Nov 29 2023 at 01:38):

Jeremy Tan said:

Yes, if you pull in the right import

:-) Here's what I've got: import Mathlib.Init.Set

Jireh Loreaux (Nov 29 2023 at 01:53):

I think Mathlib.Order.Basic might work, but I can't check. That's where the notation is defined.

Kevin Sullivan (Nov 29 2023 at 01:55):

Jireh Loreaux said:

I think Mathlib.Order.Basic might work, but I can't check. That's where the notation is defined.

Thank you, Jireh. That was it.

NO, that actually didn't work.

Jireh Loreaux (Nov 29 2023 at 01:56):

In any case, you'll most likely want to import Data.Set.Basic to have any nice theorems about sets.

Kevin Sullivan (Nov 29 2023 at 02:01):

Jireh Loreaux said:

In any case, you'll most likely want to import Data.Set.Basic to have any nice theorems about sets.

Oh of course. That's it. Funny that many but not all notations came through Init.Set. Thank you.

Jireh Loreaux (Nov 29 2023 at 02:06):

Init.Set is sort of a relic.

Last updated: Dec 20 2023 at 11:08 UTC