trim_pre — Mathlib

English

There is a relation between prehaar and index via equality in the ratio sense (eq_1).

Русский

Существует связь между prehaar и индексом через равенство (eq_1).

LaTeX

$$$\\mathrm{prehaar}(K_0,U,K) = \\mathrm{eq_1}(K_0,U,K)$$$

Lean4

/-- `MeasureTheory.OuterMeasure.mkMetric'.pre m r` is a trimmed measure provided that
`m (closure s) = m s` for any set `s`. -/
theorem trim_pre [MeasurableSpace X] [OpensMeasurableSpace X] (m : Set X → ℝ≥0∞) (hcl : ∀ s, m (closure s) = m s)
    (r : ℝ≥0∞) : (pre m r).trim = pre m r :=
  by
  refine le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)
  rw [trim_eq_iInf]
  refine
    iInf_le_of_le (closure s) <|
      iInf_le_of_le subset_closure <| iInf_le_of_le measurableSet_closure ((pre_le ?_).trans_eq (hcl _))
  rwa [diam_closure]

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