isBasis_iff_isBasis'_subset_ground

Mathlib.Combinatorics.Matroid.Basic

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

← MathLib Explorer

English

A basis I of X is equivalent to I being a Basis' of X together with X ⊆ E.

Русский

База I X эквивалентна тому, что I является Basis' I X вместе с X ⊆ E.

LaTeX

$$$ M.IsBasis I X \iff M.IsBasis' I X \land X \subseteq M.E $$$

Lean4

theorem isBasis_iff_isBasis'_subset_ground : M.IsBasis I X ↔ M.IsBasis' I X ∧ X ⊆ M.E :=
  ⟨fun h ↦ ⟨h.isBasis', h.subset_ground⟩, fun h ↦ (isBasis'_iff_isBasis h.2).mp h.1⟩

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

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

Разделы

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

Аффилиация

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