indep_iff

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

← MathLib Explorer

English

For N ≤r M, N.Indep I is equivalent to M.Indep I and I ⊆ N.E.

Русский

Для N ≤r M выполнение N.Indep I эквивалентно M.Indep I и I ⊆ N.E.

LaTeX

$$$ N.Indep I \leftrightarrow (M.Indep I \land I \subseteq N.E) $$$

Lean4

theorem indep_iff (hMN : N ≤r M) : N.Indep I ↔ M.Indep I ∧ I ⊆ N.E :=
  ⟨fun h ↦ ⟨h.of_isRestriction hMN, h.subset_ground⟩, fun h ↦ h.1.indep_isRestriction hMN h.2⟩

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

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

Разделы

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

Аффилиация

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