circuit_iff_delete_of_disjoint

Mathlib.Combinatorics.Matroid.Minor.Delete

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

← MathLib Explorer

English

If C and D are disjoint, then M.IsCircuit C iff (M \ D).IsCircuit C.

Русский

Если C и D дизjoint, то M.IsCircuit C эквивалентно (M \ D).IsCircuit C.

LaTeX

$$$ Disjoint(C,D) \Rightarrow M.IsCircuit(C) \iff (M \setminus D).IsCircuit(C) $$$

Lean4

theorem circuit_iff_delete_of_disjoint {C : Set α} (hCD : Disjoint C D) : M.IsCircuit C ↔ (M ＼ D).IsCircuit C :=
  ⟨fun h ↦ delete_isCircuit_iff.2 ⟨h, hCD⟩, fun h ↦ h.of_delete⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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