length_mono — Mathlib

English

Let f be a Stieltjes function. For any sets s1 and s2 in the real line with s1 contained in s2, the associated length is nondecreasing: length(s1) ≤ length(s2).

Русский

Пусть f — функция Стилетджеса. Для любых множеств s1 ⊆ s2 на ℝ длина, связанная с f, не уменьшается: length(s1) ≤ length(s2).

LaTeX

$$$s_1 \subseteq s_2 \quad \Rightarrow\quad f.length(s_1) \le f.length(s_2)$$$

Lean4

theorem length_mono {s₁ s₂ : Set ℝ} (h : s₁ ⊆ s₂) : f.length s₁ ≤ f.length s₂ :=
  iInf_mono fun _ => biInf_mono fun _ => h.trans

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