exists_memBaseSet_isPartition — Mathlib

English

There exists a π with MemBaseSet I c r π and π.IsPartition given distortion hc on top of π and its complement.

Русский

Существует π с MemBaseSet I c r π и π.IsPartition при заданном искажении hc.

LaTeX

$$$\\exists \\pi, l.MemBaseSet I c r \\pi ∧ \\pi.IsPartition$$$

Lean4

theorem exists_memBaseSet_isPartition (l : IntegrationParams) (I : Box ι) (hc : I.distortion ≤ c)
    (r : (ι → ℝ) → Ioi (0 : ℝ)) : ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition :=
  by
  rw [← Prepartition.distortion_top] at hc
  have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
  simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r

Похожие утверждения