## Stream: new members

### Topic: maximal finset in finset of finsets

#### 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!

#### 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?

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

#### 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?

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

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

#### Reid Barton (Sep 13 2018 at 18:47):

Sorry, not finset.map but finset.image.

#### 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⟩


Wow, thanks!

#### Mario Carneiro (Sep 13 2018 at 18:49):

That uses decidable_eq, doesn't it?

rofl

#### 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


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

#### Mario Carneiro (Sep 13 2018 at 18:50):

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

#### 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?

#### Kevin Buzzard (Sep 13 2018 at 18:51):

you can just prove this using the zorn in mathlib

#### 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

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

#### Reid Barton (Sep 13 2018 at 18:52):

decidable_eq nat doesn't use axioms either

#### Mario Carneiro (Sep 13 2018 at 18:53):

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

#### Reid Barton (Sep 13 2018 at 18:53):

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

#### Mario Carneiro (Sep 13 2018 at 18:54):

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

#### 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

#### Mario Carneiro (Sep 13 2018 at 18:54):

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

sure

#### 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


#### Mario Carneiro (Sep 13 2018 at 18:56):

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

#### Reid Barton (Sep 13 2018 at 18:56):

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

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

#### 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

#### Kenny Lau (Sep 13 2018 at 18:58):

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

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

#### 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

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

#### 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

#### Reid Barton (Sep 13 2018 at 19:08):

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

#### Mario Carneiro (Sep 13 2018 at 19:13):

is_total_preorder exists in core btw

#### Mario Carneiro (Sep 13 2018 at 19:13):

but totality is not needed

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

#### 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

#### Mario Carneiro (Sep 13 2018 at 19:16):

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

#### Mario Carneiro (Sep 13 2018 at 19:17):

that works in any total preorder

#### 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

#### 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

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

#### 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