maximal finset in finset of finsets

Stream: new members

[Bryan Gin-ge Chen]

Excuse the weird title. I'm trying to prove that a finset of subsets of a finset must contain an element of largest size, without relying on classical choice:

lemma not_empty_has_max_size {E : finset α} {F : finset (finset α)} :
F ⊆ powerset E → F ≠ ∅ → ∃ x ∈ F, ∀ g ∈ F, card g ≤ card x := sorry

Here's my attempt so far, which seems to have taken me down a strange path:

import data.finset

variable α:Type*
variable [decidable_eq α]

open finset

lemma finset.card_one_eq {E : finset α} : card E = 1 ↔ ∃ a, E = finset.singleton a :=
begin
  have h : _ := @multiset.card_eq_one α E.val,
  unfold card,
  rw [iff_congr h, exists_congr],
  intro a,
  rw [←singleton_val, val_inj],
  refl
end

lemma powerset_empty : powerset (∅ : finset α) = finset.singleton ∅ := rfl

lemma subset_singleton {F : finset (finset α)} :
F ⊆ finset.singleton (∅:finset α) ↔
F = ∅ ∨ F = finset.singleton ∅ :=
begin
  split,
  intro h,
  by_cases h1 : F = ∅,
  exact or.inl h1,
  have : F = finset.singleton ∅ := begin
    sorry
  end,
  sorry,
  intro h,
  exact or.elim h (begin
    intro h1,
    rw h1,
    simp
  end) (begin
    intro h1,
    rw h1,
    simp
  end)
end

lemma not_empty_has_max_size {E : finset α} {F : finset (finset α)} :
F ⊆ powerset E → F ≠ ∅ → ∃ x ∈ F, ∀ g ∈ F, card g ≤ card x :=
begin
  intros FPE Fne,
  induction E using finset.induction with a E ha hE,
  rw [powerset_empty, subset_singleton] at FPE,
  exact or.elim FPE (by contradiction) begin
    intro h,
    exact exists.intro ∅ begin
      rw h,
      exact exists.intro (mem_singleton_self ∅) (begin
        intros g hg,
        rw mem_singleton at hg,
        rw hg
      end)
    end
  end,
  by_cases hh1 : F ⊆ powerset E,
  exact hE hh1,
  sorry
end

I'm hoping someone can point me in a smarter direction. Thanks as always!

[Reid Barton]

Doesn't every finset of finsets contain an element of largest size, regardless of E and the associated condition?

[Bryan Gin-ge Chen]

Maybe, I got worried that without having some kind of bound on the size of the finsets I wouldn't be able to prove it without choice.

[Kevin Buzzard]

just use finset.map (I'm assuming this exists!) on finset.card to get a finset of nats and then take the max and work your way back?

[Reid Barton]

A finset is basically a list, and you could write a program that takes a list of lists and returns one of the maximum length, so there should be no trouble proving it constructively.

[Reid Barton]

Yeah, I was looking for a function on finset which is max after applying a function, but I guess since nat has decidable equality you can use finset.map in this case.

[Reid Barton]

Sorry, not finset.map but finset.image.

[Chris Hughes]

lemma not_empty_has_max_size {E : finset α} {F : finset (finset α)} :
F ⊆ powerset E → F ≠ ∅ → ∃ x ∈ F, ∀ g ∈ F, card g ≤ card x :=
λ _ h, let ⟨n, hn⟩ := (max_of_ne_empty (mt image_eq_empty.1 h) : ∃ a, a ∈ finset.max (F.image card)) in
let ⟨x, hx₁, hx₂⟩ := mem_image.1 (mem_of_max hn) in
⟨x, hx₁, hx₂.symm ▸ λ g hg, le_max_of_mem (mem_image.2 ⟨g, hg, rfl⟩) hn⟩

[Bryan Gin-ge Chen]

Wow, thanks!

[Mario Carneiro]

That uses decidable_eq, doesn't it?

[Kevin Buzzard]

rofl

[Mario Carneiro]

My suggestion:

import data.finset

section
variables {α : Type*} (r : α → α → Prop) [is_preorder α r]
local infix ` ≼ `:50 := r

theorem list_zorn : ∀ l : list α, l ≠ [] → ∃ a ∈ l, ∀ b, a ≼ b → b ≼ a := sorry
theorem finset_zorn : ∀ s : finset α, s ≠ ∅ → ∃ a ∈ s, ∀ b, a ≼ b → b ≼ a := sorry

end

[Bryan Gin-ge Chen]

I would have never thought of using finset.image. And yes, decidable_eq is allowed.

[Mario Carneiro]

here the relation is card s <= card t on finsets

[Kenny Lau]

lemma not_empty_has_max_size {E : finset α} {F : finset (finset α)} :
F ⊆ powerset E → F ≠ ∅ → ∃ x ∈ F, ∀ g ∈ F, card g ≤ card x :=
λ _ h, let ⟨n, hn⟩ := (max_of_ne_empty (mt image_eq_empty.1 h) : ∃ a, a ∈ finset.max (F.image card)) in
let ⟨x, hx₁, hx₂⟩ := mem_image.1 (mem_of_max hn) in
⟨x, hx₁, hx₂.symm ▸ λ g hg, le_max_of_mem (mem_image.2 ⟨g, hg, rfl⟩) hn⟩

what is the role of E in your theorem?

[Kevin Buzzard]

you can just prove this using the zorn in mathlib

[Mario Carneiro]

of course, but this (1) doesn't use nonconstructive axioms and (2) doesn't need the chain condition

[Bryan Gin-ge Chen]

If E is unnecessary here all the better. In the "application", it's the ground set of a matroid.

[Reid Barton]

decidable_eq nat doesn't use axioms either

[Mario Carneiro]

yes, but the theorem can be proven constructively without that assumption

[Reid Barton]

Yeah, the max/min stuff should be on multisets.

[Mario Carneiro]

Unfortunately, here max/min don't work directly since it's not a poset

[Kenny Lau]

you can have zorn on a set (i.e. type) S as long as you have a choice function on P(P(S))\{{}}, right

[Mario Carneiro]

yes, but we don't have that here and I claim it's still provable

[Kenny Lau]

sure

[Reid Barton]

I mean we should just define max for a set in the same style as prod, in terms of max on multiset, and nat is already a decidable linear whatever so there would be no problem there.

protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod

[Mario Carneiro]

what is this about nat? I don't see it in the question

[Reid Barton]

nat is the codomain of finset.card (I assume)

[Mario Carneiro]

sure but that doesn't really matter; we are doing the choosing on finset A which is not decidable (unless you assume so)

[Mario Carneiro]

all that decidability of nat gives you is decidability of the relation ≼ given by s ≼ t ↔ card s ≤ card t

[Kenny Lau]

I guess Kevin ran away from all this decidable nonsense :P

[Reid Barton]

I'm a bit confused.
All I am saying is that the original thing should be a direct conclusion of some lemma about max of a multiset nat, applied to F.1.map finset.card.

[Reid Barton]

That lemma being the analogue for multisets of finset.max_of_ne_empty and finset.le_max_of_mem

[Reid Barton]

But I guess maybe decidable_linear_order is stronger than decidable_eq anyways, so it doesn't really matter.

[Mario Carneiro]

the point is this isn't a question about decidable linear orders, but decidable preorders. Lack of uniqueness of the maximum makes it hard to define a function like max directly

[Reid Barton]

You mean something like a "pre-total order"?

[Mario Carneiro]

is_total_preorder exists in core btw

[Mario Carneiro]

but totality is not needed

[Reid Barton]

Finding the maximum value of a function on a finite set is a pretty standard thing to do. Of course there might not be a unique element of the set which maximizes the function, but the maximum value of the function is still well-defined. And often you only need some statement about the existence of a maximizing element.
It's not very obvious how you're supposed to get this from only the ability to take the maximum element of a finite set (in a totally ordered type).

[Mario Carneiro]

like kenny and chris have shown, you can take the image of the finset and get the maximum

[Mario Carneiro]

unless you care about constructivity and then you have to prove it from scratch

[Mario Carneiro]

that works in any total preorder

[Mario Carneiro]

in a partial order, I don't see any easy way to get it except zorn's lemma

[Kenny Lau]

like kenny and chris have shown, you can take the image of the finset and get the maximum

I don't think I did anything

[Bryan Gin-ge Chen]

I care a little bit about constructivity, but maybe I'll see how far I can get with Chris's solution first.

[Mario Carneiro]

oops, I didn't see that you just quoted chris's solution