map_loops

Mathlib.Combinatorics.Matroid.Loop

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

English

Under a matroid map with InjOn on the ground, the loops of the mapped matroid are exactly the image of the original loops.

Русский

Петли отображения матроидa равны образу исходных петель под отображением.

LaTeX

$$$ (M.map f hf).loops = f '' M.loops $$$

Lean4

@[simp]
theorem map_loops {f : α → β} {hf : InjOn f M.E} : (M.map f hf).loops = f '' M.loops := by simp [loops]

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

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

Разделы

Аффилиация

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