comap_loops

Mathlib.Combinatorics.Matroid.Loop

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

English

The loops of M comapped along f are exactly the preimages of the loops of M under f.

Русский

Петли матроида M после сопоставления через f равны предобразу петель M по f.

LaTeX

$$$ (M.comap f).loops = f^{-1} M.loops $$$

Lean4

@[simp]
theorem comap_loops {M : Matroid β} {f : α → β} : (M.comap f).loops = f ⁻¹' M.loops := by
  rw [loops, comap_closure_eq, image_empty, loops]

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

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

Разделы

Аффилиация

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