isFlat_closure

Mathlib.Combinatorics.Matroid.Closure

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

English

The closure of the ground equals the ground itself.

Русский

Замыкание основания равно самому основанию.

LaTeX

$$$M.closure M.E = M.E$$$

Lean4

@[simp]
theorem isFlat_closure : M.IsFlat (M.closure X) := by rw [closure, sInter_eq_iInter]; exact .iInter (·.2.1)

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

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

Разделы

Аффилиация

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