eq_of_subset_isCircuit

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCircuit.eq_of_subset_isCircuit

English

If C is a circuit and C' is a circuit with C ⊆ C', then C = C'.

Русский

Если C и C' — циклы и C ⊆ C', тогда C = C'.

LaTeX

$$$M.IsCircuit(C) \rightarrow M.IsCircuit(C') \rightarrow C' \subseteq C \rightarrow C=C'$$$

Lean4

theorem eq_of_subset_isCircuit (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (h : C ⊆ C') : C = C' :=
  hC'.eq_of_dep_subset hC.dep h

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

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

Разделы

Аффилиация

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