CompactPartition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.measurableSet_disjointed_fin line 14

Source documentation

Disjointification preserves measurability for finite ordered index sets.

theorem measurableSet_disjointed_fin {X : Type uX} [MeasurableSpace X]
    {n : ℕ} {A : Fin n → Set X} (hA : ∀ i, MeasurableSet (A i)) (i : Fin n) :
    MeasurableSet (disjointed A i) := by
…

theorem OAI.Problem356.exists_compact_small_partition line 21

Source documentation

A compact metric set admits a finite Borel partition into sets of arbitrarily small diameter. Empty cells are permitted, so the indexing is uniform.

theorem exists_compact_small_partition {X : Type uX} [MetricSpace X]
    [MeasurableSpace X] [BorelSpace X] {K : Set X} (hK : IsCompact K)
    {δ : ℝ} (hδ : 0 < δ) :
    ∃ (n : ℕ) (A : Fin n → Set X),
      (∀ i, MeasurableSet (A i)) ∧
      Pairwise (fun i j => Disjoint (A i) (A j)) ∧
      (⋃ i, A i) = K ∧
      (∀ i, A i ⊆ K) ∧
      (∀ i, ∀ x ∈ A i, ∀ y ∈ A i, dist x y < δ) := by
…

theorem OAI.Problem356.exists_compact_component_partition line 61

Source documentation

The small cells may simultaneously be chosen inside a prescribed finite family of pairwise disjoint compact components.

theorem exists_compact_component_partition {X : Type uX} [MetricSpace X]
    [MeasurableSpace X] [BorelSpace X] {ι : Type uIndex} [Fintype ι]
    (K : ι → Set X) (hK : ∀ a, IsCompact (K a))
    (hDisjoint : Pairwise (fun a b => Disjoint (K a) (K b)))
    {δ : ℝ} (hδ : 0 < δ) :
    ∃ (n : ℕ) (A : ι × Fin n → Set X),
      (∀ p, MeasurableSet (A p)) ∧
      Pairwise (fun p q => Disjoint (A p) (A q)) ∧
      (⋃ p, A p) = ⋃ a, K a ∧
      (∀ p, A p ⊆ K p.1) ∧
      (∀ p, ∀ x ∈ A p, ∀ y ∈ A p, dist x y < δ) := by
…