uniqueBaseOn_indep_iff

Mathlib.Combinatorics.Matroid.Constructions

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

← MathLib Explorer

English

If I ⊆ E, then (uniqueBaseOn I E).Indep J ↔ J ⊆ I.

Русский

Если I ⊆ E, то (uniqueBaseOn I E).Indep J ⇔ J ⊆ I.

LaTeX

$$$ (I \subseteq E) \Rightarrow (uniqueBaseOn I E).Indep J \iff J \subseteq I $$$

Lean4

theorem uniqueBaseOn_indep_iff (hIE : I ⊆ E) : (uniqueBaseOn I E).Indep J ↔ J ⊆ I :=
  by
  rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, and_iff_left_iff_imp]
  exact fun h ↦ h.trans hIE

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

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

Разделы

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

Аффилиация

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