ofTop_apply

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.ofTop_apply

English

Another instance: the diameter of the image under e equals the original diameter.

Русский

Ещё один случай: диаметр образа под e равен исходному диаметру.

LaTeX

$$$\mathrm{diam}(\mathrm{image}(e, s)) = \mathrm{diam}(s)$$$

Lean4

@[simp]
theorem ofTop_apply (h : s₁ = ⊤) (x : s₁) : (ofTop s₁ h x : P) = x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru