pre — Mathlib

English

The sequence n ↦ pre m (n^{-1}) is monotone in n.

Русский

Последовательность n ↦ pre m(n^{-1}) монотонна по n.

LaTeX

$$Monotone fun k => pre m k⁻¹$$

Lean4

/-- Auxiliary definition for `OuterMeasure.mkMetric'`: given a function on sets
`m : Set X → ℝ≥0∞`, returns the maximal outer measure `μ` such that `μ s ≤ m s`
for any set `s` of diameter at most `r`. -/
def pre (m : Set X → ℝ≥0∞) (r : ℝ≥0∞) : OuterMeasure X :=
  boundedBy <| extend fun s (_ : diam s ≤ r) => m s

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