diam_mono — Mathlib

English

If s ⊆ t and t is bounded, then diam(s) ≤ diam(t).

Русский

Если s ⊆ t и t ограничено, то diam(s) ≤ diam(t).

LaTeX

$$$s \\subseteq t \\land \\operatorname{IsBounded}(t) \\Rightarrow \\operatorname{diam}(s) \\le \\operatorname{diam}(t)$$$

Lean4

/-- If `s ⊆ t`, then the diameter of `s` is bounded by that of `t`, provided `t` is bounded. -/
theorem diam_mono {s t : Set α} (h : s ⊆ t) (ht : IsBounded t) : diam s ≤ diam t :=
  ENNReal.toReal_mono ht.ediam_ne_top <| EMetric.diam_mono h

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