inter_coloops_subset

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis'.inter_coloops_subset

← MathLib Explorer

English

If I is a basis for X, then X ∩ coloops ⊆ I.

Русский

Если I — база для X, то X ∩coloops ⊆ I.

LaTeX

$$∀ {α} {M}, {X I : Set α}, M.IsBasis' I X → X ∩ M.coloops ⊆ I$$

Lean4

theorem inter_coloops_subset (hIX : M.IsBasis' I X) : X ∩ M.coloops ⊆ I :=
  by
  intro e ⟨heX, (heI : M.IsColoop e)⟩
  rwa [← heI.mem_closure_iff_mem, hIX.isBasis_closure_right.closure_eq_right, heI.mem_closure_iff_mem]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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