lemma about when a filter is a pure filter

Stream: Is there code for X?

[Bernd Losert]

I am looking for a lemma of the form f ≤ pure x ∧ f.ne_bot → f = pure x. I can't seem to find anything of this sort. Is it just plain missing?

[David Wärn]

I think you'd expect it to be stated as example {X} (x : X) : is_atom (pure x : filter X), but library_search can't solve this so I guess it's missing?

[Floris van Doorn]

I think it's missing, but here is a proof.

import order.filter.basic

open filter set

lemma le_pure_iff_or {α : Type*} {f : filter α} {a : α} : f ≤ pure a ↔ f = pure a ∨ f = ⊥ :=
begin
  by_cases h : ∅ ∈ f,
  { simp_rw [empty_mem_iff_bot.mp h, bot_le, eq_self_iff_true, or_true] },
  { simp_rw [empty_mem_iff_bot.not.mp h, or_false, le_antisymm_iff, iff_self_and, le_pure_iff,
      pure_le_iff],
    intros haf s hsf, by_contra has, apply h, convert inter_mem haf hsf,
    rw singleton_inter_eq_empty.mpr has },
end

lemma le_pure_iff_eq {α : Type*} {f : filter α} [ne_bot f] {a : α} : f ≤ pure a ↔ f = pure a :=
by rw [le_pure_iff_or, or_iff_left (ne_bot.ne ‹_›)]

[Reid Barton]

It's basically docs#ultrafilter.unique applied to pure.
In an old version of mathlib I have lying around, it's literally ultrafilter_unique ultrafilter_pure but is_ultrafilter seems not to have survived some refactor.

[Floris van Doorn]

Oh, that is a lot nicer!

import order.filter.ultrafilter

open filter

lemma le_pure_iff_eq {α : Type*} {f : filter α} [ne_bot f] {a : α} (h : f ≤ pure a) :
  f = pure a :=
ultrafilter.unique (pure a) h

[Bernd Losert]

OK. Should I open a PR to add le_pure_iff_eq to mathlib or should I just stick with ultrafilter.unique?

[Yaël Dillies]

I think that could be a lemma, but please also the is_atom spelling.

[Bernd Losert]

Should this go under filter.ultrafilter?

[Bernd Losert]

Not sure what is_atom is about.

[Yaël Dillies]

An atom in an order is something which is not minimum but just above the minimum.

[Bernd Losert]

Interesting. First time seeing that terminology.

[Reid Barton]

If something is getting connected to is_atom it should be ultrafilter itself

[Bernd Losert]

Hmm... filter does not seem to have a order_bot instance.

[Yaël Dillies]

docs#filter.complete_lattice

[Patrick Massot]

Bernd, if Lean is asking you to provide such an instance then it probably tried to look for it too soon (eg. before understanding which type you want to consider filters on). This often come from using apply instead of refine. If this is not enough hint you should post a mwe.

[Bernd Losert]

OK. I'm running into problems when I try do:

lemma is_atom' (f : ultrafilter α) : is_atom ↑f :=

[Johan Commelin]

Try replacing ↑f by (f : filter \a)

[Bernd Losert]

Ah, that magically worked.

[Bernd Losert]

Doing f.to_filter also works. How come it gets confused with ↑f?

[Yaël Dillies]

This used to work until about 8 or 10 months ago, from my experience. I think elaboration changed a bit?

[Patrick Massot]

How could lean guess the type of ↑f?

[Patrick Massot]

There would be many coercions from ultrafilter X to many different types.

[Johan Commelin]

↑ means "insert an invisible function (aka, coercion) to some other type here"

[Patrick Massot]

That would be ambiguous on paper too.

[Yaël Dillies]

From the fact that the only coercion ultrafilter ? → filter ? is the coercion ultrafilter α → filter α.

[Yaël Dillies]

Oh wait, that does not apply here.

[Patrick Massot]

Yaël, you're adding information that is not provided to Lean here

[Bernd Losert]

There is not real context to disambiguate it though.

[Patrick Massot]

You're telling lean: I'm going to prove that "you know what I mean by f" is an atom.

[Yaël Dillies]

What I have in mind is the case of set and finset. convex ℝ s for s : finset E used to work, but now it doesn't.

[Bernd Losert]

What's the quickest way of turning ¬g = ⊥ into g.ne_bot? I am having a suprisingly hard time trying to make this conversion.

[Anne Baanen]

rw ← ne.def?

[Adam Topaz]

by squeeze_simp should give you the answer.

[Anne Baanen]

docs#ne.def

[Yaël Dillies]

Anne, this is docs#filter.ne_bot

[Bernd Losert]

ne.def does not turn it into ne_bot though.

[Yaël Dillies]

You just want \<h\> (docs#filter.ne_bot.mk)

[Bernd Losert]

It seems I have to chain ne.def and then ne_bot_iff, which seems roundabout.

[Kevin Buzzard]

import order.filter.basic

example (α : Type) (f : filter α) :
  ¬ (f = ⊥) ↔ f.ne_bot :=
⟨λ h, ⟨h⟩, λ h, h.1⟩

[Kevin Buzzard]

there are the proofs in both directions

[Bernd Losert]

I think that will be a good thing to add to mathlib's filter.basic.

[Kevin Buzzard]

filter.ne_bot is just a structure with one constructor so the proof you want is ⟨h⟩

[Adam Topaz]

Hmm... should we add the following simp lemma?

@[simp]
lemma filter.ne_bot_of_ne_bot {α : Type*} (F : filter α) :
  ¬ F = ⊥ ↔ F.ne_bot :=
⟨λ h, ⟨h⟩, λ h, h.1⟩

[Bernd Losert]

Yes please.

[Adam Topaz]

Well, my question is whether it should be a simp lemma.

[Bernd Losert]

I can add it to my PR about ultrafilter.is_atom

[Yaël Dillies]

docs#filter.ne_bot_iff

[Adam Topaz]

yeah I just saw that too

[Yaël Dillies]

Everything is already there

[Bernd Losert]

Yeah, but I need to convert f ≠ ⊥ to ¬ (f = ⊥), which is getting painful.

[Adam Topaz]

you can use docs#ne.def

[Adam Topaz]

It's annoying because the simp normal form of $a \ne b$ is \not a = b, but that filter lemma uses $a \ne \bot$

[Adam Topaz]

import order.filter.basic

@[simp]
lemma filter.ne_bot_iff_ne_bot {α : Type*} (F : filter α) :
  ¬ F = ⊥ ↔ F.ne_bot := ⟨λ h, ⟨h⟩, λ h, h.1⟩

example {α : Type*} (F : filter α) (h : F ≠ ⊥) : F.ne_bot := by simpa using h

[Adam Topaz]

But again, I don't know whether that should really be a simp lemma.

[Yaël Dillies]

Given that its use is a literal constructor application, I would say no.

[Adam Topaz]

But most of the filter lemmas that use this have filter.ne_bot as a typeclass assumption

[Bernd Losert]

Made of PR: https://github.com/leanprover-community/mathlib/pull/13171

[Eric Rodriguez]

I just realised, why do we have this as opposed to docs#ne_zero?