## Stream: new members

### Topic: Map preserving a property

#### 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


#### 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?)

#### 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,

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

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

#### Sebastián Galkin (Aug 30 2020 at 18:53):

choose made the trick. Thank you!

Last updated: May 18 2021 at 15:14 UTC