isClosed_iff_isFlat

Mathlib.Combinatorics.Matroid.Closure

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

English

For a subset F in the ground, M.subtypeClosure.IsClosed F ↔ M.IsFlat F.

Русский

Для подмножества F в основе матроида M выполнено: M.subtypeClosure.IsClosed F ⇔ M.IsFlat F.

LaTeX

$$$M.subtypeClosure.IsClosed F \iff M.IsFlat F$$$

Lean4

theorem isClosed_iff_isFlat {F : Iic M.E} : M.subtypeClosure.IsClosed F ↔ M.IsFlat F := by simp [subtypeClosure]

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

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

Разделы

Аффилиация

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