symm

Mathlib.Topology.MetricSpace.Congruence

URI: https://scilib.ai/kg/mathlib#Congruent.symm

English

Symmetry of the congruence relation: if v1 ≅ v2, then v2 ≅ v1.

Русский

Симметричность отношения конгруэнции: если v1 эквивалентно v2, то v2 эквивалентно v1.

LaTeX

$$Congruent v1 v2 → Congruent v2 v1$$

Lean4

@[symm]
protected theorem symm (h : v₁ ≅ v₂) : v₂ ≅ v₁ := fun i₁ i₂ ↦ (h i₁ i₂).symm

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

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

Разделы

Аффилиация

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