instNonemptySubtypeSetIsBase

Mathlib.Combinatorics.Matroid.Basic

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

English

There exists a base B of M, i.e., there is a B ⊆ α with M.IsBase B.

Русский

Существует база B для матроида M, то есть существует подмножество B ⊆ α такое, что M.IsBase B.

LaTeX

$$$$ \exists B \subseteq \alpha, M.IsBase B $$$$

Lean4

instance (M : Matroid α) : Nonempty { B // M.IsBase B } :=
  nonempty_subtype.2 M.exists_isBase

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

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

Разделы

Аффилиация

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