ediam_image — Mathlib

English

For any subset s of α, the diameter with respect to the EMetric is preserved by an isometry: EMetric.diam(h''s) = EMetric.diam(s).

Русский

Для произвольного подмножества s пространства α диаметр по метрике EMetric сохраняется при образе под изометрией.

LaTeX

$$$\operatorname{EMetric}.\operatorname{diam}(h''s) = \operatorname{EMetric}.\operatorname{diam}(s)$$$

Lean4

@[simp]
theorem ediam_image (h : α ≃ᵢ β) (s : Set α) : EMetric.diam (h '' s) = EMetric.diam s :=
  h.isometry.ediam_image s

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