Zulip Chat Archive

Stream: new members

Topic: defining set of triples


view this post on Zulip Manuel Candales (Mar 30 2021 at 14:42):

Hi, I have a question regarding sets and cartesian products. I can define a set like this: let A := {s : ℝ×ℝ×ℝ | s ≠ (0, 0, 0)},. However, if I try to define that same set like this: let A := {(x, y, z) : ℝ×ℝ×ℝ | (x, y, z) ≠ (0, 0, 0)}, I get an error. Am I using the wrong notation? How do I go about defining something like: {(x, y, z) : ℝ×ℝ×ℝ | x > 1 ∧ y ≠ 0 ∧ z < 1}.

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 14:45):

You can do {s : ℝ×ℝ×ℝ | s.1 > 1 ∧ s.2.1 ≠ 0 ∧ s.2.2 < 1}. It's a bit crap I know -- in Lean 4 there will be more flexibility with this kind of thing. Or you could probably do some trick with let (x, (y, z)) := s in... after the | which might look nicer to read, but would end up harder to work with.

view this post on Zulip Manuel Candales (Mar 30 2021 at 14:46):

Thanks! By the way, is that a \mid or a pipe?

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 14:48):

For set notation it's just the | button on my keyboard (so I guess a pipe). The \| is different -- this is used for "divides" in number theory (so I guess a \mid).

view this post on Zulip Damiano Testa (Mar 30 2021 at 14:50):

Alternatively, this also works:

example : set (××) := {s : ×× |  (x y z : ), s = (x, y, z)  x > 1  y  0  z < 1}

I am not sure if it is any better, though.

view this post on Zulip Manuel Candales (Mar 30 2021 at 14:52):

Thank! I think I will use that last one. The goal reads much better with the exists condition.

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:53):

You can use a match statement probably.... this should be much easier in lean4 IIRC

view this post on Zulip Damiano Testa (Mar 30 2021 at 14:53):

Yes, depending on how many conditions you want to impose, the extra rfls may be worth the effort! :smile:

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:55):

import data.real.basic

example : set (××) := {s : ×× | match s with | (x, y, z) := x > 1  y  0  z < 1 end}

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:56):

Although that's a bit of a mouthful

view this post on Zulip Damiano Testa (Mar 30 2021 at 14:56):

I guess that the conclusion is that there are a few workarounds, but no clear winner!

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:59):

Here's Kevin's suggestion:

import data.real.basic

example : set (××) := {s : ×× | let (x,y,z) := s in x > 1  y  0  z < 1}

view this post on Zulip Eric Wieser (Mar 30 2021 at 14:59):

Is there some way to use docs#set.has_sep here?

view this post on Zulip Eric Wieser (Mar 30 2021 at 15:00):

No, I guess that's only useful for filtering sets that aren't just set.univ

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 18:26):

My concern with the match and let options is that we're defining data here and it might leave a real mess. If this were going in mathlib I would use the ugly s.2.1 definition and then define a refl lemma mem_thenameoftheset_iff unwinding it.


Last updated: May 12 2021 at 23:13 UTC