eq_of_dep_subset

Mathlib.Combinatorics.Matroid.Circuit

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

English

If C is a circuit and X ⊆ C with Dep(X), then X = C.

Русский

Если C — цикл и X ⊆ C и Dep(X), тогда X = C.

LaTeX

$$$M.IsCircuit(C) \rightarrow M.Dep(X) \rightarrow X \subseteq C \rightarrow X = C$$$

Lean4

theorem eq_of_dep_subset (hC : M.IsCircuit C) (hX : M.Dep X) (hXC : X ⊆ C) : X = C :=
  hC.eq_of_not_indep_subset hX.not_indep hXC

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

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

Разделы

Аффилиация

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