Stream: math-comp users

Topic: Filter {set A+B} to get {set A}


view this post on Zulip Julin Shaji (Apr 02 2024 at 05:44):

Given a {set A+B} value, is there a way to filter it to get a value of type {set A}?

view this post on Zulip Julin Shaji (Apr 02 2024 at 05:49):

Kind of like this list version?

Fixpoint getLeft {A B: Type} (l: seq (A + B)): seq A :=
  match l with
  | [::] => [::]
  | (inl a) :: l' => a :: getLeft l'
  | _ :: l' => getLeft l'
  end.

view this post on Zulip Julin Shaji (Apr 02 2024 at 05:49):

But since we can't do pattern match on sets, I wasn't sure how to go about this.

view this post on Zulip Julin Shaji (Apr 02 2024 at 05:51):

Tried like [set x in ab | is_inl x]. but that's still {set A+B}.

view this post on Zulip Quentin VERMANDE (Apr 02 2024 at 11:28):

Mathematically, this would be the union, for x in ab, of \{a\} if x is inl a and \emptyset otherwise.
Nevertheless, if you know an element of A, it is probably better to filter the set (as you did) and map its element by sending inr _ to your distinguished element of A.

view this post on Zulip Cyril Cohen (Apr 02 2024 at 11:35):

Quentin's right, and you can also write it in one go: given X : {set A + B} you can probably write [set a | inl a \in X].

view this post on Zulip Cyril Cohen (Apr 02 2024 at 11:36):

also known as inl @^-1: X

view this post on Zulip Cyril Cohen (Apr 02 2024 at 11:36):

(the preimage of X by inl)

view this post on Zulip Julin Shaji (Apr 03 2024 at 06:08):

Thanks!

view this post on Zulip Julin Shaji (Apr 03 2024 at 06:22):

What does \{a\} mean? It's not latex stuff, is it?

view this post on Zulip Julin Shaji (Apr 03 2024 at 06:23):

if you know an element of A, it is probably better to filter the set (as you did) and map its element by sending inr _ to your distinguished element of A.

I didn't get this part. Why do we need to have a particular element of A?

view this post on Zulip Quentin VERMANDE (Apr 03 2024 at 07:01):

Ah, yes, sorry, it is indeed LaTeX stuff, you can ignore the backslashes, I meant the singleton containing a.
You would do your map with a function from A+B to A. This function does not know that your set contains only elements of the form inl _, so you need to define where to send inputs of the form inr _, hence the distinguished element of A.


Last updated: Jul 23 2024 at 20:01 UTC