Function with fewer elements

Stream: new members

[Jérémie Turcotte]

I have a function f between two fintypes, the first of which has cardinality at least 2 smaller the the second. I want to extract 2 (distinct) elements from the 2nd type which are not in the image of f. I could prove it, but I was wondering if there was anything like this in mathlib already, given that it seems like a pretty basic thing. Thanks!

[Jérémie Turcotte]

I have no idea what to even search to find something like this in the library

[Matt Diamond]

are there any criteria for these elements other than "not in the image of f"? what should the behavior be if there are more than 2 elements not in the image?

[Jérémie Turcotte]

I really have no restrictions, I would then by using those 2 elements to find a contradiction (in some sort of pigeonhole-type argument). I just want to show there exists 2 such distinct elements, if there are more I just need 2 of them (and I don't mind if its not computable or such).

[Matt Diamond]

oh I see what you're getting at... you just want the proof that a function from a fintype of lesser cardinality leaves a number of elements out of the image

[Matt Diamond]

I don't have an answer off the top of my head, but are you aware of https://leanprover-community.github.io/mathlib_docs/combinatorics/pigeonhole.html?

[Jérémie Turcotte]

Yeah, I guess one could for instance apply finset.exists_card_fiber_lt_of_card_lt_mul twice, but seems a bit convoluted for this simple application. My guess is that someone must have a more directly application result.

[Junyan Xu]

You just want to show the complement of the range has cardinality at least 2 (using docs#finset.card_univ_diff and docs#finset.card_image_le), then you can use docs#finset.one_lt_card.

[Eric Wieser]

You can get the set as fintype.univ.filter (λ a, ∀ b, a ≠ f b)

[Eric Wieser]

You won't actually be able to extract the two elements separately computably, but you can probably turn them into a sym2 with a bit of effort.

[Yaël Dillies]

docs#finset.univ rather

[Patrick Johnson]

Defining a function and proving that it does what you want are distinct things. Since you don't worry about computability, the function can be defined using classical epsilon:

import tactic

noncomputable def fn {α β : Type*} (f : α → β) : option (β × β) :=
classical.epsilon $ λ (b : option (β × β)), ∃ (b₁ b₂ : β),
b = some (b₁, b₂) ∧ b₁ ≠ b₂ ∧ ¬∃ (a : α), f a = b₁ ∨ f a = b₂

To make some use of it, you would need to prove that in the case of [fintype α] [fintype β] (h : fintype.card α + 2 ≤ fintype.card β) it satisfies the condition.

[Praneeth Kolichala]

Is this what you want roughly?

import tactic.linarith
example {α β : Type*} [fintype α] [fintype β] [decidable_eq α]
  [decidable_eq β] (h : fintype.card α + 2 ≤ fintype.card β) (f : α → β) :
  ∃ a b, a ∉ finset.univ.image f  ∧ b ∉ finset.univ.image f ∧ a ≠ b :=
begin
  simp only [← finset.mem_compl, ← finset.one_lt_card_iff, finset.card_compl],
  zify [finset.card_le_univ],
  linarith [(show (finset.univ.image f).card ≤ fintype.card α, from finset.card_image_le)],
end

[Jérémie Turcotte]

Thanks everyone for your comments! I ended up slightly reformulating my lemma but did something quite close to Junyan Xu's suggestion