ground_nonempty

Mathlib.Combinatorics.Matroid.Basic

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

English

If M is a matroid with a nonempty instance, then its ground set E is nonempty.

Русский

Если матроид M обладает ненулевой структурой, то его множество E непусто.

LaTeX

$$$$ M.E \neq \varnothing $$$$

Lean4

theorem ground_nonempty (M : Matroid α) [M.Nonempty] : M.E.Nonempty :=
  Nonempty.ground_nonempty

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

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

Разделы

Аффилиация

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