choose from complement

Stream: new members

[Yakov Pechersky]

Do we have something simple for this?

import ring_theory.polynomial.symmetric
import ring_theory.polynomial.homogeneous
import data.mv_polynomial.basic
import data.multiset.basic

open finset

example {α : Type*} [fintype α] (s : finset α) (hs : s.card < (univ : finset α).card) :
  ∃ y : α, y ∉ s := sorry

[Yakov Pechersky]

It's like a simple rephrasing of pigeonhole.

[Ruben Van de Velde]

Can you get something about (s^c).card from hs?

[Adam Topaz]

You can use docs#set.card_lt_card

[Adam Topaz]

And docs#set.exists_of_ssubset

[Adam Topaz]

Oh wait, the first lemma goes the wrong way (and it was for fintypes anyway)

[Adam Topaz]

Going with Ruben's suggestion, there's this: docs#finset.card_compl

[Adam Topaz]

And you can deduce from that the the cardinality of the complement is positive, then use docs#finset.card_pos

[Yakov Pechersky]

Brutal. OK, thanks!

[Adam Topaz]

You probably need to use docs#finset.card_univ for some glue

[Adam Topaz]

Yeah it's not ideal...

[Yakov Pechersky]

  /-
  α : Type u_1,
  _inst_1 : fintype α,
  n : ℕ,
  x : α
  ⊢ n < fintype.card α → (∃ (v : finset α), v.card = n.succ ∧ x ∈ v)
  -/
  induction n with n IH,
  { intro _,
    use {x},
    simp },
  { intro hn,
    obtain ⟨s, hs, hm⟩ := IH ((nat.lt_succ_self _).trans hn),
    obtain ⟨y, hy⟩ : ∃ y : α, y ∉ s,
      { have hsc : sᶜ.card = fintype.card α - n.succ,
          { rw [card_compl, hs] },
        have hpos : 0 < sᶜ.card := hsc.symm ▸ nat.sub_pos_of_lt hn,
        obtain ⟨y, hy⟩ := card_pos.mp hpos,
        use y,
        simpa using hy },
    replace hy : disjoint s {y} := by simpa using hy,
    use (s ∪ {y}),
    simp [hy, hm, hs] }

[Yakov Pechersky]

Thanks!

[Ruben Van de Velde]

For your example:

import data.fintype.basic
import order.boolean_algebra

open finset

example {α : Type*} [fintype α] [decidable_eq α] (s : finset α) (hs : s.card < (univ : finset α).card) :
  ∃ y : α, y ∉ s :=
begin
  simp_rw ←finset.mem_compl,
  apply finset.card_pos.mp,
  rw [finset.card_compl],
  apply nat.sub_pos_of_lt,
  rwa ←finset.card_univ,
end

I wonder why we don't have nat.sub_pos for the iff to match docs#sub_pos - we have nat.sub_pos_of_lt in core and nat.lt_of_sub_pos in mathlib