Zulip Chat Archive

Stream: new members

Topic: Map preserving a property


view this post on Zulip Sebastián Galkin (Aug 29 2020 at 21:16):

I need to construct a set starting from some other set and a a function to map over the elements. How can I preserve the properties the function guarantees?

variables {α β : Type*}
variables (s : set α) (p : α  β  Prop)

example (f:  a,  b, p a b) :
     res: set (α × β),  x: α × β, x  res \to p x.1 x.2 := sorry

view this post on Zulip Reid Barton (Aug 29 2020 at 21:37):

I'm guessing you want something other than {ab | p ab.1 ab.2}? (Or the empty set, for that matter?)

view this post on Zulip Reid Barton (Aug 29 2020 at 21:38):

You can use mathlib's choose tactic to pick a choice function: choose f hf using f,

view this post on Zulip Sebastián Galkin (Aug 29 2020 at 21:57):

What I want to do is to use f at every element of s to produce a new set with \a s and \b s, but still retain somehow the fact that the elements of the new set have the property p.

I'll look into choose, thank you.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 22:00):

choose gives you a function F : alpha -> beta such that p a (F a) is always true, and it's easy from there.

view this post on Zulip Sebastián Galkin (Aug 30 2020 at 18:53):

choose made the trick. Thank you!


Last updated: May 18 2021 at 15:14 UTC