comap_isNonloop_iff — Mathlib

English

For a map f : α → β, (M.comap f).IsNonloop e iff M.IsNonloop (f e).

Русский

Для отображения f : α → β, (M.comap f).IsNonloop e эквивалентно M.IsNonloop (f e).

LaTeX

$$$(M.comap f).IsNonloop e \leftrightarrow M.IsNonloop (f e)$$$

Lean4

@[simp]
theorem comap_isNonloop_iff {M : Matroid β} {f : α → β} : (M.comap f).IsNonloop e ↔ M.IsNonloop (f e) := by
  rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton, and_iff_left (injOn_singleton _ _)]

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