contract_eq_self_iff

Mathlib.Combinatorics.Matroid.Minor.Contract

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

English

M / C equals M if and only if C is disjoint from the ground E: M / C = M ⇔ C ∩ E = ∅.

Русский

M / C = M тогда и только тогда, когда C не пересекает грунт E: C ∩ E = ∅.

LaTeX

$$$ M / C = M \\iff C \\cap E = \\varnothing $$$

Lean4

theorem contract_eq_self_iff : M ／ C = M ↔ Disjoint C M.E := by
  rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]

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

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

Разделы

Аффилиация

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