exists_isBasis'

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.exists_isBasis'

← MathLib Explorer

English

For any X there exists I such that I is a Basis' I X.

Русский

Для любого X существует I такое, что I — Basis' I X.

LaTeX

$$$ \exists I, M.IsBasis' I X $$$

Lean4

theorem exists_isBasis' (M : Matroid α) (X : Set α) : ∃ I, M.IsBasis' I X :=
  let ⟨_, hI, _⟩ := M.empty_indep.subset_isBasis'_of_subset (empty_subset X)
  ⟨_, hI⟩

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

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

Разделы

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

Аффилиация

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