uniqueBaseOn_rankPos

Mathlib.Combinatorics.Matroid.Constructions

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

← MathLib Explorer

English

If I ⊆ E and I is nonempty, then RankPos of uniqueBaseOn I E holds.

Русский

Если I ⊆ E и I непусто, то RankPos(uniqueBaseOn I E).

LaTeX

$$$I \subseteq E \land I \neq \varnothing \Rightarrow \mathrm{RankPos}(\mathrm{uniqueBaseOn}(I,E))$$$

Lean4

theorem uniqueBaseOn_rankPos (hIE : I ⊆ E) (hI : I.Nonempty) : RankPos (uniqueBaseOn I E) where
  empty_not_isBase := by simpa [uniqueBaseOn_isBase_iff hIE] using Ne.symm <| hI.ne_empty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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