subset_ground

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCocircuit.subset_ground

English

A cocircuit is contained in the ground set: C ⊆ E.

Русский

Кококрит содержится в множестве основания: C ⊆ E.

LaTeX

$$$\text{IsCocircuit}_M(C) \Rightarrow C \subseteq M.E$$$

Lean4

@[aesop unsafe 10% (rule_sets := [Matroid])]
theorem subset_ground (hC : M.IsCocircuit C) : C ⊆ M.E :=
  hC.isCircuit.subset_ground

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

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

Разделы

Аффилиация

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