defining set of triples

Stream: new members

[Manuel Candales]

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}.

[Kevin Buzzard]

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.

[Manuel Candales]

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

[Kevin Buzzard]

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).

[Damiano Testa]

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.

[Manuel Candales]

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

[Adam Topaz]

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

[Damiano Testa]

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

[Adam Topaz]

import data.real.basic

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

[Adam Topaz]

Although that's a bit of a mouthful

[Damiano Testa]

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

[Adam Topaz]

Here's Kevin's suggestion:

import data.real.basic

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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.