map_id

Mathlib.Combinatorics.Matroid.Map

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

English

Mapping by the identity map preserves the matroid: M.map id (injOn_id M.E) = M.

Русский

Отображение по тождественному отображению сохраняет матроид: M.map id (injOn_id M.E) = M.

LaTeX

$$$ M.map\ id\ (injOn\ id\ M.E) = M $$$

Lean4

@[simp]
theorem map_id : M.map id (injOn_id M.E) = M := by simp [ext_iff_indep]

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

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

Разделы

Аффилиация

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