Mapping into a finset product

Stream: Is there code for X?

[George Shakan]

I would like to define a function into a Cartesian product. What I do not know is how to work with the elements of a Cartesian product.

import data.finset.basic
import data.real.basic


open_locale classical pointwise

example (A B : finset ℝ ) : A.card = 1 :=
begin
  let f : A.product B := λ x , x.1.product x.2

end

[Eric Wieser]

Can you write down what you're trying to do in maths? This looks like an #xy problem

[Eric Wieser]

let f : A.product B := λ x , x.1.product x.2 is about as nonsensical as let n : ℕ := λ x, 3 * x

[George Shakan]

Sure, I am trying to prove Ruzsa's triangle inequality. To do so, I am trying to define various functions from Cartesian products. For instance, the main point of the proof is to define a tricky f : (A- B) X C -> (A-C) X (B-C) and show it is an injection.

[Eric Wieser]

What does - mean there?

[Yaël Dillies]

docs#finset.has_sub

[Yaël Dillies]

The thing is that what you're talking about is not really a function, George.

[Yaël Dillies]

This is because you first have to write c in A - B as a - b with a ∈ A and b ∈ B.

[Yaël Dillies]

You would be better off using a double counting argument.

[Yaël Dillies]

(which is really the "proper" way of writing what you're trying to do)

[George Shakan]

Sure, I can try it this way, but still I am curious about the original question

[Yaël Dillies]

I would first define f : α → α → α → α := λ a b c, (a - c, b - c), then consider λ x : α × α, f (first_witness x.1) (second_witness x.1) x.2.

[Eric Wieser]

To answer the original question, I think either of these has a suitable type:

variables (A B C : finset X)

def f (x : ↥(A - B) × ↥C) : ↥(A-C) × ↥(B-C) :=
⟨⟨_, _⟩, ⟨_, _⟩⟩ -- use x.1, x.1.prop, x.2, x.2.prop etc
--^      ^ data here

def g (x : ↥((A - B).product C)) : ↥((A-C).product (B-C)) :=
⟨⟨_, _⟩, ⟨_, _⟩⟩ -- use x.1.1, x.prop.1, x.1.2, x.prop.2 etc
--^  ^   data here

[Yaël Dillies]

Missing some noncomputables here and there :wink:

[Kyle Miller]

Seemed like a fun challenge doing it directly; here's a tactic mode definition (not recommended! this is a first draft)

import data.finset.basic
import data.finset.pointwise
import data.real.basic
import tactic

open_locale pointwise

noncomputable
def f (A B C : finset ℝ) : (A - B).product C → (A - C).product (B - C) :=
begin
  intro p,
  have hp := p.2,
  rw [finset.mem_product, finset.mem_sub] at hp,
  cases hp with hp1 hp2,
  choose a b hp1 using hp1,
  use (a - p.1.2, b - p.1.2),
  rw [finset.mem_product, finset.mem_sub],
  split,
  { use [a, p.1.2, hp1.1, hp2], },
  { rw [finset.mem_sub],
    use [b, p.1.2, hp1.2.1, hp2], },
end