getting started proving filter.ne_bot

Stream: maths

[Bernd Losert]

I want to prove this:

example (ℬ : filter_basis X) (∅ ∉ ℬ) : ℬ.filter.ne_bot := begin

end

I don't see anything remotely like this in mathlib, which surprises me. How do I get started with this proof? I don't even see a theorem about ne_bot iff empty set is not a member of the filter.

[Adam Topaz]

docs#has_basis.eq_bot_iff

[Adam Topaz]

docs#has_basis.ne_bot_iff

[Adam Topaz]

docs#filter_basis.has_basis

[Adam Topaz]

Those should get you most of the way there.

[Bernd Losert]

The first two links are 404.

[Adam Topaz]

fixed

[Bernd Losert]

I don't get the has_basis stuff because it involves some kind of indexing set. What's that about?

[Adam Topaz]

you don't need to worry about that, just use filter_basis.has_basis to know that the filter associated to the basis satisfies has_basis for the given basis.

[Bernd Losert]

OK. I'll give it a shot. Thanks.

[Adam Topaz]

Here's a proof that can probably be golfed to a single line:

import order.filter.bases

variables {X : Type*}

example (ℬ : filter_basis X) (h : ∅ ∉ ℬ) : ℬ.filter.ne_bot := begin
  rw ℬ.has_basis.ne_bot_iff,
  intros i hh,
  rw ← set.ne_empty_iff_nonempty,
  intros c,
  apply h,
  dsimp at c,
  rwa c at hh,
end

[Bernd Losert]

It's going to take me a long time to be able code golf tactics.

[Adam Topaz]

You might want to replace your assumption that B doesn't contain empty with something like the assumption in docs#filter.has_basis.ne_bot_iff

[Adam Topaz]

That would probably make it smoother to use your lemma in practice.

[Bernd Losert]

OK. The indexing stuff was confusing me, so I was avoiding it.

[Adam Topaz]

The indexing stuff is because the definition of has_basis prefers the collection of sets defining the basis for the filter to be indexed by some auxiliary type $\iota$.

[Bernd Losert]

Do you know why they made it that way?

[Patrick Massot]

Bernd, a lot of bases are naturally indexed. For instance neighborhoods in metric spaces have a basis of balls indexed by positive radii.

[Patrick Massot]

And because Adam wanted it:

example {X : Type*} (ℬ : filter_basis X) (h : ∅ ∉ ℬ) : ℬ.filter.ne_bot :=
ℬ.has_basis.ne_bot_iff.mpr (λ u hu, ne_empty_iff_nonempty.mp $ λ H : u = ∅, h $ H ▸ hu)

[Bernd Losert]

Alright. Thanks guys.