congruent_comm

Mathlib.Topology.MetricSpace.Congruence

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

English

Congruence is symmetric: v1 ≅ v2 iff v2 ≅ v1.

Русский

Конгруэнция симметрична: v1 ≅ v2 эквивалентно v2 ≅ v1.

LaTeX

$$$v_1\cong v_2 \;\Leftrightarrow\; v_2\cong v_1$$$

Lean4

theorem _root_.congruent_comm : v₁ ≅ v₂ ↔ v₂ ≅ v₁ :=
  ⟨Congruent.symm, Congruent.symm⟩

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

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

Разделы

Аффилиация

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