ext

Mathlib.Combinatorics.SimpleGraph.Dart

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Dart.ext

English

If d1.toProd = d2.toProd, then d1 = d2.

Русский

Если d1.toProd = d2.toProd, значит d1 = d2.

LaTeX

$$$ d_1.toProd = d_2.toProd \Rightarrow d_1 = d_2 $$$

Lean4

@[ext]
theorem ext (d₁ d₂ : G.Dart) (h : d₁.toProd = d₂.toProd) : d₁ = d₂ :=
  (Dart.ext_iff d₁ d₂).mpr h

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

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

Разделы

Аффилиация

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