ultrafilter is principal if it contains a finite set

Stream: Is there code for X?

[Kyle Miller]

Does this already exist somewhere? and if not, what would be a nice way to prove it?

lemma ultrafilter.eq_principal_of_finite_mem (f : ultrafilter α) (s : set α) (h : s.finite) (h' : s ∈ f) :
  ∃ x, (f : filter α) = principal {x} :=
begin
  sorry
end

[Kevin Buzzard]

In an ultrafilter, for every subset s of alpha, either s is in or its complement is in. That sounds useful. Is the pullback of an ultrafilter along an injection an ultrafilter again?

[Kevin Buzzard]

Maybe you don't want to promote s to a type though

[Kyle Miller]

The proof I had in mind (but didn't want to write) was to say there exists a minimal finite set in the ultrafilter, and so long as that finite set has cardinality greater than one, there's a minimal-er one.

[Kevin Buzzard]

A consequence of the "t is in or t.compl is in" is that for a finite collection of subsets, either one is in or the intersection of the complements is in

[Kevin Buzzard]

And now apply with the elements of your s

[Mario Carneiro]

You can do it by finset.induction: prove that if s \in f then there exists x such that {x} \in f. If s \cup {a} \in f, then either {a} \in f (and we are done) or s \in f and apply the IH

[Kevin Buzzard]

That's nice, and hopefully the right induction principle is there

[Mario Carneiro]

actually docs#finite.induction_on is a bit more convenient here

[Mario Carneiro]

Actually, you can do this without induction by using docs#ultrafilter.finite_bUnion_mem_iff and docs#set.bUnion_of_singleton

[Mario Carneiro]

you could strengthen the theorem to say \exists x \in s, (f : filter α) = principal {x} too

[Oliver Nash]

There should also be a route using docs#function.argmin_on I expect Mario's suggestion will be more efficient but function.argmin_on may allow you to express the proof you had in mind more directly.

[Oliver Nash]

I guess it would start something like:

import order.filter.ultrafilter

open filter

variables {α : Type*} (f : ultrafilter α)

lemma ultrafilter.eq_principal_of_finite_mem (s : set α) (h : s.finite) (h' : s ∈ f) :
  ∃ x ∈ s, (f : filter α) = principal {x} :=
begin
  let F : set (finset α) := { t | (t : set α) ∈ f },
  have hF : F.nonempty := ⟨h.to_finset, by simpa only [set.finite.coe_to_finset, set.mem_set_of_eq]⟩,
  let t := function.argmin_on finset.card nat.lt_wf F hF,
  -- etc.
  sorry
end