comap_loopyOn

Mathlib.Combinatorics.Matroid.Map

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

English

The comap of a loopyOn set with f equals loopyOn of the preimage.

Русский

Комап loopyOn(E) по f равен loopyOn(f^{-1}(E)).

LaTeX

$$comap (loopyOn E) f = loopyOn (preimage f E)$$

Lean4

@[simp]
theorem comap_loopyOn (f : α → β) (E : Set β) : comap (loopyOn E) f = loopyOn (f ⁻¹' E) := by rw [eq_loopyOn_iff]; aesop

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

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

Разделы

Аффилиация

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