restrictSubtype_ground

Mathlib.Combinatorics.Matroid.Map

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

English

The ground set of the restricted matroid equals the universal set.

Русский

Множество оснований ограниченного матроида равно все множество.

LaTeX

$$$(M.restrictSubtype X).E = \mathrm{univ}$$$

Lean4

@[simp]
theorem restrictSubtype_ground : (M.restrictSubtype X).E = univ := by simp [restrictSubtype]

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

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

Разделы

Аффилиация

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