hasBasis_toFilteriUnion_top — Mathlib

English

For the top prepartition, the HasBasis structure for toFilteriUnion top is given similarly with π.IsPartition.

Русский

Для верхнего разбиения HasBasis для toFilteriUnion верхнего уровня задаётся аналогично с π.IsPartition.

LaTeX

$$$(l.toFilteriUnion I \\top).HasBasis (\\lambda r. l.RCond (r)) (\\\\{\\pi | ∃ c, l.MemBaseSet I c (r c) \\pi ∧ π.IsPartition})$$$

Lean4

theorem hasBasis_toFilteriUnion_top (l : IntegrationParams) (I : Box ι) :
    (l.toFilteriUnion I ⊤).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c)) fun r =>
      {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition} :=
  by
  simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using l.hasBasis_toFilteriUnion I ⊤

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