uniqueBaseOn_finitary

Mathlib.Combinatorics.Matroid.Constructions

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

← MathLib Explorer

English

The matroid uniqueBaseOn I E is finitary.

Русский

Матроид, заданный как uniqueBaseOn I E, является финиитарным.

LaTeX

$$[Finitary](uniqueBaseOn I E)$$

Lean4

instance uniqueBaseOn_finitary : Finitary (uniqueBaseOn I E) :=
  by
  refine ⟨fun K hK ↦ ?_⟩
  simp only [uniqueBaseOn_indep_iff'] at hK ⊢
  exact fun e heK ↦ singleton_subset_iff.1 <| hK _ (by simpa) (by simp)

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

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

Разделы

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

Аффилиация

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