closure_subset_ground

Mathlib.Combinatorics.Matroid.Closure

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

← MathLib Explorer

English

If X ⊆ Y, then closure X ⊆ closure Y.

Русский

Если X ⊆ Y, то closure X ⊆ closure Y.

LaTeX

$$$X \subseteq Y \Rightarrow M.closure X \subseteq M.closure Y$$$

Lean4

@[aesop unsafe 10% (rule_sets := [Matroid])]
theorem closure_subset_ground (M : Matroid α) (X : Set α) : M.closure X ⊆ M.E :=
  sInter_subset_of_mem ⟨M.ground_isFlat, inter_subset_right⟩

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

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

Разделы

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

Аффилиация

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