rankPos_nonempty

Mathlib.Combinatorics.Matroid.Basic

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

← MathLib Explorer

English

If M has RankPos, then M is nonempty.

Русский

Если у M есть RankPos, то M непуст.

LaTeX

$$$$ \text{RankPos} \Rightarrow M.Nonempty $$$$

Lean4

instance rankPos_nonempty {M : Matroid α} [M.RankPos] : M.Nonempty :=
  by
  obtain ⟨B, hB⟩ := M.exists_isBase
  obtain rfl | ⟨e, heB⟩ := B.eq_empty_or_nonempty
  · exact False.elim <| RankPos.empty_not_isBase hB
  exact ⟨e, M.subset_ground B hB heB⟩

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

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

Разделы

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

Аффилиация

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