isBasis_self_iff_indep

Mathlib.Combinatorics.Matroid.Basic

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

← MathLib Explorer

English

If I is a Basis' I X, then I is a Basis I (X ∩ E).

Русский

Если I является Basis' I X, то I является базой I (X ∩ E).

LaTeX

$$$ M.IsBasis' I X \Rightarrow M.IsBasis I (X \cap M.E) $$$

Lean4

@[simp]
theorem isBasis_self_iff_indep : M.IsBasis I I ↔ M.Indep I :=
  by
  rw [isBasis_iff', and_iff_right rfl.subset, and_assoc, and_iff_left_iff_imp]
  exact fun hi ↦ ⟨fun _ _ ↦ subset_antisymm, hi.subset_ground⟩

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

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

Разделы

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

Аффилиация

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