Filter from properties preserved under countable union

Stream: Is there code for X?

[Josha Dekker]

Suppose that we have 'p : Set X -> Prop' which carries over to subsets (hmono) and is preserved under countable unions (hcountable_union). The set of sets whose complement satisfy this property defines a Filter (with the countable intersection property); the finite union version of this is used in proving IsCompact.induction_on, and I'm using the countable union version of this to prove IsLindelof.induction_on. Are these results already added separately/is there interest in adding them separately? See the following:

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

universe u v
variable {X : Type u}
variable [TopologicalSpace X]
variable {α : Type u} {s : Set X}

example {p : Set X → Prop} (he : p ∅)
    (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
    (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃ s ∈ S, s)) :
    Filter X := by
  let f : Filter X :=
    { sets := { t | p tᶜ }
      univ_sets := by simpa
      sets_of_superset := fun ht₁ ht ↦ hmono (compl_subset_compl.2 ht) ht₁
      inter_sets := by
        intro ht₁ ht₂
        simp only [mem_setOf_eq, compl_inter]
        intro p₁ p₂
        let Se : Set (Set X) := {ht₁ᶜ, ht₂ᶜ}
        have hSe : Se.Countable := by simp
        have : ∀ s ∈ Se, p s := by
          rintro _ ⟨rfl|_⟩
          · exact p₁
          · have h : _ = ht₂ᶜ := by
              assumption
            rw [h]
            exact p₂
        have := hcountable_union Se hSe this
        have : ⋃ s∈ Se, s = ht₁ᶜ ∪ ht₂ᶜ := by simp
        rwa [← this]
        }
  have : CountableInterFilter f := by
    apply CountableInterFilter.mk
    simp only [Filter.mem_mk, mem_setOf_eq, compl_sInter, sUnion_image]
    intro S hS hsp
    let f := fun (x : Set X) ↦ xᶜ
    let S' := f '' S
    have hsp : ∀ s ∈ S', p s := by simpa
    have hS' : S'.Countable := Countable.image hS _
    have : ⋃ s ∈ S, sᶜ = ⋃ s ∈ S', s := by simp
    rw [this]
    apply hcountable_union S' hS' hsp
  exact f

[Josha Dekker]

This was suggested in the reviewing process of #9107

[Kevin Buzzard]

My gut feeling is that if this is useful for you in some project doing interesting mathematics then this is a good justification for adding them. If you're taking complements everywhere then maybe you're looking for ideals not filters though (do we have them?)

[Josha Dekker]

In essence the complements are not necessary here, the more general set-up would I guess be that I can introduce 4 related results, which feel more intuitive in terms of Filters for me (also because the direct use-cases are for filters, that saves some intermediate results).

A: CountableInterFilter from sets {t : p t} if p is stable under countable intersections
B: CountableInterFilter from sets {t : p tᶜ} if p is stable under countable unions, infer from A
C: filter from sets {t : p tᶜ} if p is stable under finite unions
D: filter from sets {t : p t} if p is stable under finite intersections, infer from C

I think this should carry over to more general unions/intersections as well, but I'm not sure how useful that will be.

Shall I add A and B to Filter/CountableInter.lean and C and D to Filter/Basic.lean?

[Michael Rothgang]

My understanding of the mathlib way is that "if you can generalise something at no cost (to e.g. the proofs), then do it". (This may be different from writing textbooks or math papers.) In other words: this seems plausible to me.

[Kevin Buzzard]

@Josha Dekker you could try making a PR with just C and D, and you might learn something from the reviews. Making a PR is usually the best way to get the experts to think about your ideas.

[Josha Dekker]

Okay, I'll do that! Thank you!

[Josha Dekker]

This is now #9200, any remarks are welcome! I found that proving C and D separately was quicker than inferring either from the other.

[Yury G. Kudryashov]

I left some comments there.

[Josha Dekker]

Thanks, I’ll take a look soon!