Sections of a set in a product

Stream: Is there code for X?

[Felix Weilacher]

By a (vertical) section of a set a : Set X \times Y, I mean a set of the form {y : Y | (x,y) \in a} for some x : X.

Is there a good way to talk about these? I have been using a.curry x and it sometimes works as desired, but gives me some issues. For example I'm not sure how to fix the following error.

theorem mem_curry {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    y ∈ (a.curry x) ↔ (x, y) ∈ a := sorry
-- failed to synthesize instance Membership β (β → Prop)

[Patrick Massot]

This spelling is bound to bring pain on you.

[Patrick Massot]

It is violating the abstraction barrier of the definition of Set.

[Patrick Massot]

Did you try simply using Prod.mk x ⁻¹' a?

[Kyle Miller]

You can write it like this too:

theorem mem_curry {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    y ∈ (x, ·) ⁻¹' a ↔ (x, y) ∈ a := Set.mem_preimage

[Kyle Miller]

This has some nice symmetry:

example {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    y ∈ (x, ·) ⁻¹' a ↔ (x, y) ∈ a := Set.mem_preimage

example {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    x ∈ (·, y) ⁻¹' a ↔ (x, y) ∈ a := Set.mem_preimage

[Patrick Massot]

Oh yes, (x, ·) ⁻¹' a definitely reads better than Prod.mk x ⁻¹' a and has the nice benefit of working just as well with the right-hand set.

[Patrick Massot]

Yeah, I mean this symmetry.

[Floris van Doorn]

Oh, the parentheses of a pair also counts as parentheses surrounding ·? That's pretty neat

[Felix Weilacher]

Kyle Miller said:

This has some nice symmetry:

example {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    y ∈ (x, ·) ⁻¹' a ↔ (x, y) ∈ a := Set.mem_preimage

example {α β : Type*} {a : Set (α × β)} (x : α) (y : β) :
    x ∈ (·, y) ⁻¹' a ↔ (x, y) ∈ a := Set.mem_preimage

Thanks! I will probably switch to this

[Felix Weilacher]

BTW, by rfl works in stead of Set.mem_preimage for the proof, but rfl doesn't.

[Kyle Miller]

Oh, that's because rfl is for Eq. You can use Iff.rfl here too.

[Floris van Doorn]

(or .rfl)

[Felix Weilacher]

thanks again