inter_ground_subset_closure

Mathlib.Combinatorics.Matroid.Closure

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

English

The closure of a set is flat.

Русский

Замыкание множества является плоскостью (flat).

LaTeX

$$$M.IsFlat (M.closure X)$$$

Lean4

theorem inter_ground_subset_closure (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X := by
  simp_rw [closure_def, subset_sInter_iff]; simp

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

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

Разделы

Аффилиация

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