isBasis_iff

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.IsRestriction.isBasis_iff

← MathLib Explorer

English

Under N ≤r M, N.IsBasis I X holds iff M.IsBasis I X and X ⊆ N.E.

Русский

При N ≤r M база N.IsBasis I X эквивалентна M.IsBasis I X и X ⊆ N.E.

LaTeX

$$N.IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ N.E$$

Lean4

theorem isBasis_iff (hMN : N ≤r M) : N.IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ N.E :=
  ⟨fun h ↦ ⟨h.of_isRestriction hMN, h.subset_ground⟩, fun h ↦ h.1.isBasis_isRestriction hMN h.2⟩

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

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

Разделы

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

Аффилиация

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