comap_isLoop_iff — Mathlib

English

For any f, an element e is a loop in the comap of M along f if and only if f(e) is a loop in M.

Русский

Для любого отображения f элемент e является петлей в компапе M вдоль f тогда и только тогда, когда f(e) — петля в M.

LaTeX

$$$ (M.comap f).IsLoop e \iff M.IsLoop (f e) $$$

Lean4

@[simp]
theorem comap_isLoop_iff {M : Matroid β} {f : α → β} : (M.comap f).IsLoop e ↔ M.IsLoop (f e) := by simp [isLoop_iff]

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