Zulip Chat Archive

Stream: new members

Topic: maximal finset in finset of finsets


view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 18:36):

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!

view this post on Zulip Reid Barton (Sep 13 2018 at 18:39):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 18:41):

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.

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 18:44):

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?

view this post on Zulip Reid Barton (Sep 13 2018 at 18:45):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 18:47):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 18:47):

Sorry, not finset.map but finset.image.

view this post on Zulip Chris Hughes (Sep 13 2018 at 18:48):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 18:48):

Wow, thanks!

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:49):

That uses decidable_eq, doesn't it?

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 18:50):

rofl

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:50):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 18:50):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:50):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 18:51):

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?

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 18:51):

you can just prove this using the zorn in mathlib

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:51):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 18:52):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 18:52):

decidable_eq nat doesn't use axioms either

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:53):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 18:53):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:54):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 18:54):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:54):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 18:55):

sure

view this post on Zulip Reid Barton (Sep 13 2018 at 18:55):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:56):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 18:56):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:57):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 18:58):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 18:58):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 18:59):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 19:00):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 19:03):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:07):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 19:08):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:13):

is_total_preorder exists in core btw

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:13):

but totality is not needed

view this post on Zulip Reid Barton (Sep 13 2018 at 19:14):

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).

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:15):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:16):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:17):

that works in any total preorder

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:17):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 19:22):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2018 at 19:23):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 19:56):

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


Last updated: May 11 2021 at 23:11 UTC