not_ssubset

Mathlib.Combinatorics.Matroid.Circuit

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

English

If two circuits C and C' exist, then C' is not a proper subset of C.

Русский

Если существуют два цикла C и C', то C' не является корректной подпоследовательностью C.

LaTeX

$$$M.IsCircuit(C) \rightarrow M.IsCircuit(C') \rightarrow \neg (C' ⊊ C)$$$

Lean4

theorem not_ssubset (hC : M.IsCircuit C) (hC' : M.IsCircuit C') : ¬C' ⊂ C := fun h' ↦
  h'.ne (hC.eq_of_dep_subset hC'.dep h'.subset)

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

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

Разделы

Аффилиация

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