closure_univ

Mathlib.Combinatorics.Matroid.Closure

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

English

Closure is monotone with respect to inclusion.

Русский

Замыкание монотонно по включению.

LaTeX

$$$\text{Monotone}(M.closure)$$$

Lean4

@[simp]
theorem closure_univ (M : Matroid α) : M.closure univ = M.E := by
  rw [← closure_inter_ground, univ_inter, closure_ground]

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

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

Разделы

Аффилиация

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