Is there a name for this notion?

Stream: Is there code for X?

[Ching-Tsun Chou]

Is there a name for the notion Foo defined below?

def Foo {ι α : Type*} (f : ι → Set α) (s : Set α) :=
  ∀ i : ι, (f i ∩ s).Nonempty → f i ⊆ s

[Violeta Hernández]

I don't think so. My best guess is that this is somewhat similar to quotients. Specifically, you might want some equivalence relation r on α, and to prove that r x y → x ∈ f i → y ∈ f i, so as to then lift the f i to the quotient.

[Violeta Hernández]

What do you want this for?

[Damiano Testa]

Maybe I'm misunderstanding, but what if f is the constant function to Univ, s is a singleton and alpha has at least 2 elements?

[Damiano Testa]

Ah, I thought that := was :! In my defense, I'm on mobile and it is beyond the edge!

[Damiano Testa]

Modifying a bit, it seems like you are saying that s and sᶜ form a collection of upper bounds for the subsets indexed by f.

[Damiano Testa]

This makes me think of refinements.

[Ching-Tsun Chou]

I want to prove the results given in examples below. I'm wondering whether there are standard names for Foo and Bar. Of course, it would be even better if the results are already in mathlib.

variable {ι α : Type*}

def Foo (f : ι → Set α) (s : Set α) : Prop :=
  ∀ i : ι, (f i ∩ s).Nonempty → f i ⊆ s

def Bar (f : ι → Set α) : Prop :=
  ∀ x : α, ∃ i : ι, x ∈ f i

variable {f : ι → Set α} {s : Set α}

example (h : Foo f s) : Foo f sᶜ := by
  sorry

example (ha : Bar f) (hs : Foo f s) :
    s = ⋃ i ∈ {i | (f i ∩ s).Nonempty}, f i := by
  sorry

[Damiano Testa]

Here are possible proofs. I made not attempt at minimization.

import Mathlib

variable {ι α : Type*}

def Foo (f : ι → Set α) (s : Set α) : Prop :=
  ∀ i : ι, (f i ∩ s).Nonempty → f i ⊆ s

def Bar (f : ι → Set α) : Prop :=
  ∀ x : α, ∃ i : ι, x ∈ f i

variable {f : ι → Set α} {s : Set α}

theorem Foo.iff_or : Foo f s ↔ ∀ i, f i ≤ s ∨ f i ≤ sᶜ where
  mp h := by
    unfold Foo at h
    intro i
    by_cases hi : ∃ a, a ∈ f i ∩ s
    · left
      obtain ⟨a, ha⟩ := hi
      apply h
      use a
    aesop
  mpr h := by
    unfold Foo
    intro i hi
    obtain (hf | hf) := h i
    · assumption
    · cases hi with
    | intro a ha =>
      tauto_set

-- This is an `↔` with the same proof.
example (h : Foo f s) : Foo f sᶜ := by
  grind [compl_compl, Foo.iff_or]

example (ha : Bar f) (hs : Foo f s) :
    s = ⋃ i ∈ {i | (f i ∩ s).Nonempty}, f i := by
  unfold Bar at ha
  ext x
  simp only [Foo.iff_or, Set.le_eq_subset, Set.mem_setOf_eq, Set.mem_iUnion, exists_prop] at hs ⊢
  constructor
  · intro hx
    obtain ⟨i, hi⟩ := ha x
    grind only [Set.inter_nonempty]
  · rintro ⟨w, hi, hx⟩
    grind only [Set.inter_nonempty, Set.inter_nonempty_iff_exists_right, = Set.subset_def,
    = Set.mem_compl_iff, #dd14, #a1a0, #57dc, #e5ff, #7662, #9ba1]

[Ching-Tsun Chou]

The proof I came up with:

open Set

variable {ι α : Type*}

def Saturates (f : ι → Set α) (s : Set α) : Prop :=
  ∀ i : ι, (f i ∩ s).Nonempty → f i ⊆ s

def IsAmple (f : ι → Set α) : Prop :=
  ∀ x : α, ∃ i : ι, x ∈ f i

variable {f : ι → Set α} {s : Set α}

theorem saturates_compl (h : Saturates f s) : Saturates f sᶜ := by
  rintro i ⟨_, _⟩ y _ _
  have h_y : (f i ∩ s).Nonempty := by use y; grind
  grind [h i h_y]

theorem union_of_isAmple_saturates (ha : IsAmple f) (hs : Saturates f s) :
    s = ⋃ i ∈ {i | (f i ∩ s).Nonempty}, f i := by
  ext x
  simp only [mem_setOf_eq, mem_iUnion, exists_prop]
  constructor
  · intro h_x
    obtain ⟨i, _⟩ := ha x
    use i, ⟨x, by grind⟩, by grind
  · rintro ⟨i, h_i, _⟩
    grind [hs i h_i]

[Yury G. Kudryashov]

For IsAmple, we usually write ⋃ i, f i = univ.

[Jakub Nowak]

I think IsAmple is equivalent to CompactExhaustion on discrete topology? It's a bad idea to define it like that, but maybe name like Exhausts or IsExhaustion would make sense?

[Jakub Nowak]

Ah, wait, nvm, it's not the same because of condition subset_interior_succ'.

[Jakub Nowak]

You could also call it Covers or IsCovering: https://en.wikipedia.org/wiki/Cover_(topology)

[Jakub Nowak]

Isn't Foo equivalent to saying that s is a member of set algebra generated by { f i | i }? MeasureTheory.generateSetAlgebra
Hm, not really, you would also need infinite union, not just finite.

[Jakub Nowak]

Maybe you could call notion Foo as saying that s is generated by f (under infinite unions).
Nvm, as you noticed in union_of_isAmple_saturates, s is generated by f only if f is a covering.

[Ching-Tsun Chou]

I did end up renaming IsAmple to IsCover:
https://github.com/leanprover/cslib/pull/268
Some background on why I want to prove these simple results: they capture the essence of a key step in the proof of the closure of ω-regular languages under complementation. See the statement of lemma 2.2 and the discussion following it (but not the proof) on pages 139-140 of this document:
thomas-survey.pdf

[Jakub Nowak]

Do you need these as a separate definitions? As an example there's docs#TopologicalSpace.ofClosed and it just has arguments like ∀ A, A ⊆ T → ⋂₀ A ∈ T and ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T inlined, without defining separate notions like ClosedUnderInifiteIntersection or ClosedUnderUnion. If the definition is short enough it's possible there's no need to create a separate notion.

[Jakub Nowak]

So instead of coming up with a new notion like "satures" it might be easier to just call it subset_of_inter_nonempty.

[Ching-Tsun Chou]

I can probably get rid of IsCover. But I think defining Saturates makes the statement of saturates_compl much clearer than simply inlining the definition.

[Jakub Nowak]

How about this instead of IsRegular.fin_cover_saturates:?

theorem IsRegular.fin_iUnion {I : Type*} (I' : Set I) [Finite I]
    {p : I → ωLanguage Symbol} (hr : ∀ i ∈ I', (p i).IsRegular) : (⋃ i ∈ I', p i}).IsRegular

[Jakub Nowak]

You could even drop Finite I for I'.Finite I think.

[Ching-Tsun Chou]

That is not the theorem I want and it does not suffice for the proving the closure of ω-regular languages under complementation. In fact, I already have basically that result as the theorem IsRegular.iSup earlier in the same file.

[Jakub Nowak]

Yeah, true, I think I'm lacking context to help you more.