base_iff

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

← MathLib Explorer

English

For N ≤r M, N.IsBase B is equivalent to M.IsBasis B N.E.

Русский

Для N ≤r M: N.IsBase B эквивалентно M.IsBasis B N.E.

LaTeX

$$N.IsBase B ↔ M.IsBasis B N.E$$

Lean4

theorem base_iff (hMN : N ≤r M) {B : Set α} : N.IsBase B ↔ M.IsBasis B N.E :=
  ⟨fun h ↦ IsBase.isBasis_of_isRestriction h hMN, fun h ↦ by simpa [hMN.eq_restrict] using h.restrict_isBase⟩

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

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

Разделы

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

Аффилиация

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