dist_div_eq_dist_mul_left

Mathlib.Analysis.Normed.Group.Uniform

URI: https://scilib.ai/kg/mathlib#dist_div_eq_dist_mul_left

← MathLib Explorer

English

The distance of a/b to c equals the distance of a to c⋅b.

Русский

Расстояние между a/b и c равно расстоянию между a и c⋅b.

LaTeX

$$$\\operatorname{dist}(\\tfrac{a}{b}, c) = \\operatorname{dist}(a, c\\cdot b)$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_div_eq_dist_mul_left (a b c : E) : dist (a / b) c = dist a (c * b) := by
  rw [← dist_mul_right _ _ b, div_mul_cancel]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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