outer_le_length — Mathlib

English

For every subset s of ℝ, the Stieltjes outer measure does not exceed the corresponding length: f.outer(s) ≤ f.length(s).

Русский

Для каждого подмножества s ⊆ ℝ внешняя мера Стилетджеса не превосходит соответствующую длину: f.outer(s) ≤ f.length(s).

LaTeX

$$f.outer(s) \le f.length(s)$$

Lean4

theorem outer_le_length (s : Set ℝ) : f.outer s ≤ f.length s :=
  OuterMeasure.ofFunction_le _

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