Specialising forall_neBot_le_iff to countable intersection

Stream: Is there code for X?

[Josha Dekker]

Hi, is there a way to specialise the result Ultrafilter.forall_neBot_le_iff (https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Order/Filter/Ultrafilter.lean#L473-L477) to require only the Countable Intersection property? See the below MWE for my approach; I have one step that I cannot manage to fill in because I'm not sure how to deal with the coercions here (my experience with these is (severely) lacking; I did the math and thought the result should be correct, but it could be I'm missing some small condition?

The relevance is in my PR for Lindelöf spaces: #9107. I'm trying to also get an ultrafilter characterisation for Lindelöf spaces, and figured that this result would be an important step for that.

import Mathlib.Data.Set.Countable
import Mathlib.Order.Filter.CountableInter
import Mathlib.Topology.Compactness.Compact

open Set Filter

universe u v
variable {α : Type u}

theorem Ultrafilter.countable_intersection_forall_neBot_le_iff {g : Filter α} {p : Filter α → Prop}
  (hp : Monotone p) : (∀ f : Filter α, CountableInterFilter f → NeBot f → f ≤ g → p f) ↔
  ∀ f : Ultrafilter α, CountableInterFilter f.toFilter → ↑f ≤ g → p f := by
  refine' ⟨fun H f _ hf => H f _ f.neBot hf, _⟩
  · assumption
  intro H f a hf hfg
  apply hp
  · apply Ultrafilter.of_le f
  · apply H
    refine { countable_sInter_mem := ?countable_sInter_mem }
    · have := a.countable_sInter_mem
      sorry
    · apply (Ultrafilter.of_le f).trans hfg

[Yury G. Kudryashov]

Is there a version of Ultrafilter.exists_le for filters with countable intersections?

[Josha Dekker]

I'm not aware of this. I originally thought that I needed this to get some of the results in #9107 working, but I have bypassed the result in some of the more important usages by directly proving the required results.

[Pedro Sánchez Terraf]

Josha Dekker said:

I'm trying to also get an ultrafilter characterisation for Lindelöf spaces, and figured that this result would be an important step for that.

I'm trying to understand the statement of your theorem, does it mention $\sigma$-complete ultrafilters on a set? The existence of non-principal ones requires large cardinals (perhaps you are well-aware of this).

[Josha Dekker]

Pedro Sánchez Terraf said:

Josha Dekker said:

I'm trying to also get an ultrafilter characterisation for Lindelöf spaces, and figured that this result would be an important step for that.

I'm trying to understand the statement of your theorem, does it mention $\sigma$-complete ultrafilters on a set? The existence of non-principal ones requires large cardinals (perhaps you are well-aware of this).

The theorem as written was more of a hopeful guess: I thought the result was correct when I sketched the proof, but I couldn't find any reference for it. I couldn't close the above argument, so I thought something was missing/I was missing some insight. You are right that it does not mention sigma-complete ultrafilters, I didn't think of including these. I'm not too strong with ultrafilters anyway, so perhaps I should leave that aspect open (especially as I couldn't find an ultrafilter characterisation of Lindelöf spaces online...)