instRankPosOfNonemptyOfLoopless

Mathlib.Combinatorics.Matroid.Loop

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

English

If M is nonempty and loopless, then RankPos M holds (the matroid has positive rank).

Русский

Если M непуст и без петель, то у M положительный ранг.

LaTeX

$$$$ \text{RankPos}(M) \text{ при } M.\text{Nonempty} \land M.\text{Loopless}. $$$$

Lean4

instance {M : Matroid α} [M.Nonempty] [Loopless M] : RankPos M :=
  M.ground_nonempty.elim fun _ he ↦ (isNonloop_of_loopless he).rankPos

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

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

Разделы

Аффилиация

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