similar_comm

Mathlib.Topology.MetricSpace.Similarity

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

English

If v1 ∼ v2 then v2 ∼ v1; the scaling is inverted.

Русский

Если v1 подобно v2, то v2 подобно v1; масштаб является обратным.

LaTeX

$$Similar.symm: if v1 ∼ v2 then v2 ∼ v1 with the same scaling inverted via reciprocal.$$

Lean4

theorem _root_.similar_comm : v₁ ∼ v₂ ↔ v₂ ∼ v₁ :=
  ⟨Similar.symm, Similar.symm⟩

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

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

Разделы

Аффилиация

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