freeOn_rankPos

Mathlib.Combinatorics.Matroid.Constructions

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

English

If E is nonempty, then RankPos of freeOn E holds.

Русский

Если E непусто, то RankPos матроида freeOn(E) истинно.

LaTeX

$$$ E.\,Nonempty \Rightarrow RankPos (freeOn E) $$$

Lean4

theorem freeOn_rankPos (hE : E.Nonempty) : RankPos (freeOn E) := by simp [rankPos_iff, hE.ne_empty.symm]

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

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

Разделы

Аффилиация

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