eq_dual_comm

Mathlib.Combinatorics.Matroid.Dual

URI: https://scilib.ai/kg/mathlib#Matroid.eq_dual_comm

English

M₁ = M₂✶ is equivalent to M₂ = M₁✶.

Русский

Матрёда: M₁ = M₂✶ эквивалентно M₂ = M₁✶.

LaTeX

$$M1 = M2.dual ↔ M2 = M1.dual$$

Lean4

theorem eq_dual_comm {M₁ M₂ : Matroid α} : M₁ = M₂✶ ↔ M₂ = M₁✶ := by rw [← dual_inj, dual_dual, eq_comm]

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

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

Разделы

Аффилиация

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