Map preserving a property

Stream: new members

[Sebastián Galkin]

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]

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

[Reid Barton]

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

[Sebastián Galkin]

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]

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]

choose made the trick. Thank you!