hasBasis_toFilterDistortion — Mathlib

English

For the top prepartition π0 = ⊤, the filter (l.toFilterDistortioniUnion I c ⊤) has a basis as above with π.iUnion = ⊤ iUnion.

Русский

Для верхнего разбиения π0 = ⊤ фильтр (l.toFilterDistortioniUnion I c ⊤) имеет базис аналогично предыдущему с π.iUnion = ⊤.

LaTeX

$$$(l.toFilterDistortioniUnion I c \\top).HasBasis l.RCond \\; (\\lambda r. {\\pi \\mid l.MemBaseSet I c r \\pi \\land \\pi.iUnion = π.iUnion_{Top}})$$$

Lean4

theorem hasBasis_toFilterDistortion (l : IntegrationParams) (I : Box ι) (c : ℝ≥0) :
    (l.toFilterDistortion I c).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π} :=
  hasBasis_biInf_principal'
    (fun _ hr₁ _ hr₂ =>
      ⟨_, hr₁.min hr₂, fun _ => MemBaseSet.mono _ le_rfl le_rfl fun _ _ => min_le_left _ _, fun _ =>
        MemBaseSet.mono _ le_rfl le_rfl fun _ _ => min_le_right _ _⟩)
    ⟨fun _ => ⟨1, Set.mem_Ioi.2 zero_lt_one⟩, fun _ _ => rfl⟩

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