ext_iff

Mathlib.Combinatorics.SimpleGraph.Dart

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

English

Two Darts are equal iff their toProd values are equal.

Русский

Две стрелы равны тогда и только тогда, когда их значения toProd равны.

LaTeX

$$$ d_1 = d_2 \iff d_1.toProd = d_2.toProd $$$

Lean4

theorem ext_iff (d₁ d₂ : G.Dart) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd := by cases d₁; cases d₂; simp

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

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

Разделы

Аффилиация

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