fundCircuit_subset_insert

Mathlib.Combinatorics.Matroid.Circuit

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

English

If e ∈ X, then fundCircuit e X = {e}.

Русский

Если e ∈ X, то fundCircuit e X = {e}.

LaTeX

$$$e\in X \Rightarrow M.fundCircuit e X = \{e\}$$$

Lean4

theorem fundCircuit_subset_insert (M : Matroid α) (e : α) (I : Set α) : M.fundCircuit e I ⊆ insert e I :=
  insert_subset_insert inter_subset_left

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

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

Разделы

Аффилиация

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