Analytic sets in the sense of a paved space

TODO: we use IsCompactSystem, which corresponds to semi-compact pavings for D-M. We use this and not compact pavings (which would be the same, but for arbitrary intersections instead of countable ones), because it's sufficient for our applications, and because it's easier to work with.

Copied from a newer Mathlib. To be deleted when we bump.

def Set.dissipate {α : Type u_1} {β : Type u_2} [LE α] (s : α → Set β) (x : α) : Set β

dissipate s is the intersection of s y for y ≤ x.

Equations

• Set.dissipate s x = ⋂ (y : α), ⋂ (_ : y ≤ x), s y

theorem Set.dissipate_def {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} : dissipate s x = ⋂ (y : α), ⋂ (_ : y ≤ x), s y

@[simp]

theorem Set.mem_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} {z : β} : z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y

theorem Set.dissipate_subset {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x y : α} (hy : y ≤ x) : dissipate s x ⊆ s y

theorem Set.iInter_subset_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] (x : α) : ⋂ (i : α), s i ⊆ dissipate s x

theorem Set.antitone_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : Antitone (dissipate s)

theorem Set.dissipate_subset_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] {x y : α} (h : y ≤ x) : dissipate s x ⊆ dissipate s y

@[simp]

theorem Set.biInter_dissipate {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} {x : α} : ⋂ (y : α), ⋂ (_ : y ≤ x), dissipate s y = dissipate s x

@[simp]

theorem Set.iInter_dissipate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : ⋂ (x : α), dissipate s x = ⋂ (x : α), s x

@[simp]

theorem Set.dissipate_bot {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] (s : α → Set β) : dissipate s ⊥ = s ⊥

@[simp]

theorem Set.dissipate_zero_nat {β : Type u_2} (s : ℕ → Set β) : dissipate s 0 = s 0

@[simp]

theorem Set.dissipate_succ {α : Type u_1} (s : ℕ → Set α) (n : ℕ) : dissipate s (n + 1) = dissipate s n ∩ s (n + 1)

theorem MeasureTheory.Set.dissipate_eq_iInter_Iic {β : Type u_4} (s : ℕ → Set β) (n : ℕ) : Set.dissipate s n = ⋂ y ∈ Finset.Iic n, s y

theorem isCompactSystem_isCompact_isClosed {𝓧 : Type u_1} [TopologicalSpace 𝓧] : IsCompactSystem fun (K : Set 𝓧) => IsCompact K ∧ IsClosed K

theorem isCompactSystem_isCompact {𝓧 : Type u_1} [TopologicalSpace 𝓧] [T2Space 𝓧] : IsCompactSystem fun (K : Set 𝓧) => IsCompact K

theorem IsCompactSystem.mono {𝓚 : Type u_3} {q q' : Set 𝓚 → Prop} (hq : IsCompactSystem q) (h_mono : ∀ (s : Set 𝓚), q' s → q s) : IsCompactSystem q'

def MeasureTheory.memProd {𝓧 : Type u_1} {𝓚 : Type u_3} (p : Set 𝓧 → Prop) (q : Set 𝓚 → Prop) : Set (𝓧 × 𝓚) → Prop

Product of two sets of sets.

Equations

• MeasureTheory.memProd p q s = ∃ (A : Set 𝓧) (B : Set 𝓚), p A ∧ q B ∧ s = A ×ˢ B

theorem MeasureTheory.memProd_prod {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {A : Set 𝓧} {B : Set 𝓚} (hp : p A) (hq : q B) : memProd p q (A ×ˢ B)

theorem MeasureTheory.memProd.mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {p' : Set 𝓧 → Prop} (hp : ∀ (s : Set 𝓧), p s → p' s) {q' : Set 𝓚 → Prop} (hq : ∀ (s : Set 𝓚), q s → q' s) {s : Set (𝓧 × 𝓚)} (hs : memProd p q s) : memProd p' q' s

def MeasureTheory.memSigma {𝓧 : Type u_1} (p : Set 𝓧 → Prop) : Set 𝓧 → Prop

The set is a countable union of sets that satisfy the property.

Equations

• MeasureTheory.memSigma p s = ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), p (A n)) ∧ s = ⋃ (n : ℕ), A n

theorem MeasureTheory.memSigma_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (hs : p s) : memSigma p s

theorem MeasureTheory.memSigma.union {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s t : Set 𝓧} (hs : memSigma p s) (ht : memSigma p t) : memSigma p (s ∪ t)

def MeasureTheory.memDelta {𝓧 : Type u_1} (p : Set 𝓧 → Prop) : Set 𝓧 → Prop

The set is a countable intersection of sets that satisfy the property.

Equations

• MeasureTheory.memDelta p s = ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), p (A n)) ∧ s = ⋂ (n : ℕ), A n

theorem MeasureTheory.memDelta_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (hs : p s) : memDelta p s

def MeasureTheory.memProdSigmaDelta {𝓧 : Type u_1} {𝓚 : Type u_3} (p : Set 𝓧 → Prop) (q : Set 𝓚 → Prop) : Set (𝓧 × 𝓚) → Prop

The set is a countable intersection of countable unions of sets that can be written as a product of two sets, each satisfying a property.

Equations

• MeasureTheory.memProdSigmaDelta p q = MeasureTheory.memDelta (MeasureTheory.memSigma (MeasureTheory.memProd p q))

def MeasureTheory.memFiniteInter {𝓧 : Type u_1} (p : Set 𝓧 → Prop) : Set 𝓧 → Prop

The set is a finite intersection of sets that satisfy the property.

Equations

• MeasureTheory.memFiniteInter p s = ∃ (t : Finset ℕ) (A : ℕ → Set 𝓧), (∀ n ∈ t, p (A n)) ∧ s = ⋂ n ∈ t, A n

theorem MeasureTheory.memFiniteInter_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (hs : p s) : memFiniteInter p s

theorem MeasureTheory.memFiniteInter.inter {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s t : Set 𝓧} (hs : memFiniteInter p s) (ht : memFiniteInter p t) : memFiniteInter p (s ∩ t)

def MeasureTheory.memFiniteUnion {𝓧 : Type u_1} (p : Set 𝓧 → Prop) : Set 𝓧 → Prop

The set is a finite union of sets that satisfy the property.

Equations

• MeasureTheory.memFiniteUnion p s = ∃ (t : Finset ℕ) (A : ℕ → Set 𝓧), (∀ n ∈ t, p (A n)) ∧ s = ⋃ n ∈ t, A n

theorem MeasureTheory.memFiniteUnion_of_prop {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s : Set 𝓧} (hs : p s) : memFiniteUnion p s

theorem MeasureTheory.memFiniteUnion.union {𝓧 : Type u_1} {p : Set 𝓧 → Prop} {s t : Set 𝓧} (hs : memFiniteUnion p s) (ht : memFiniteUnion p t) : memFiniteUnion p (s ∪ t)

theorem MeasureTheory.memProdSigmaDelta_iff {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {s : Set (𝓧 × 𝓚)} : memProdSigmaDelta p q s ↔ ∃ (A : ℕ → ℕ → Set 𝓧) (K : ℕ → ℕ → Set 𝓚) (_ : ∀ (n m : ℕ), p (A n m)) (_ : ∀ (n m : ℕ), q (K n m)), s = ⋂ (n : ℕ), ⋃ (m : ℕ), A n m ×ˢ K n m

theorem MeasureTheory.memProdSigmaDelta_of_prop {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {s : Set 𝓧} {t : Set 𝓚} (hs : p s) (hq : q t) : memProdSigmaDelta p q (s ×ˢ t)

theorem MeasureTheory.memProdSigmaDelta.mono {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} {p' : Set 𝓧 → Prop} (hp : ∀ (s : Set 𝓧), p s → p' s) {q' : Set 𝓚 → Prop} (hq : ∀ (s : Set 𝓚), q s → q' s) {s : Set (𝓧 × 𝓚)} (hs : memProdSigmaDelta p q s) : memProdSigmaDelta p' q' s

theorem MeasureTheory.memDelta_iff_of_inter {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (hp : ∀ (s t : Set 𝓧), p s → p t → p (s ∩ t)) {s : Set 𝓧} : memDelta p s ↔ ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), p (A n)) ∧ Antitone A ∧ s = ⋂ (n : ℕ), A n

theorem MeasureTheory.memSigma_iff_of_union {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (hp : ∀ (s t : Set 𝓧), p s → p t → p (s ∪ t)) {s : Set 𝓧} : memSigma p s ↔ ∃ (A : ℕ → Set 𝓧), (∀ (n : ℕ), p (A n)) ∧ Monotone A ∧ s = ⋃ (n : ℕ), A n

theorem IsCompactSystem.memProd {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} (hp : IsCompactSystem p) (hq : IsCompactSystem q) : IsCompactSystem (MeasureTheory.memProd p q)

theorem IsCompactSystem.memFiniteInter {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (hp : IsCompactSystem p) : IsCompactSystem (MeasureTheory.memFiniteInter p)

theorem IsCompactSystem.memFiniteUnion {𝓧 : Type u_1} {p : Set 𝓧 → Prop} (hp : IsCompactSystem p) : IsCompactSystem (MeasureTheory.memFiniteUnion p)

theorem MeasureTheory.fst_iInter_of_memFiniteUnion_memProd_of_antitone {𝓧 : Type u_1} {𝓚 : Type u_3} {p : Set 𝓧 → Prop} {q : Set 𝓚 → Prop} (hq : IsCompactSystem q) {B : ℕ → Set (𝓧 × 𝓚)} (hB_anti : Antitone B) (hB : ∀ (n : ℕ), memFiniteUnion (memProd p q) (B n)) : Prod.fst '' ⋂ (n : ℕ), B n = ⋂ (n : ℕ), Prod.fst '' B n