uniqueBaseOn_inter_ground_eq

Mathlib.Combinatorics.Matroid.Constructions

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

← MathLib Explorer

English

UniqueBaseOn on I ∩ E equals UniqueBaseOn I E.

Русский

UniqueBaseOn на I ∩ E равен UniqueBaseOn I E.

LaTeX

$$$ uniqueBaseOn (I \cap E)\, E = uniqueBaseOn I E $$$

Lean4

theorem uniqueBaseOn_inter_ground_eq (I E : Set α) : uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E :=
  by
  simp only [uniqueBaseOn, restrict_eq_restrict_iff, freeOn_indep_iff, subset_inter_iff]
  tauto

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

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

Разделы

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

Аффилиация

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