map_indep_iff — Mathlib

English

Independence in the mapped matroid is equivalent to independence of the preimage and equality to the image of I with respect to the mapping.

Русский

Независимость в отображенном матроидe эквивалентна независимости предобраза и равенству образа I относительно отображения.

LaTeX

$$$(M.map f hf).Indep I \iff \exists I_0, M.Indep I_0 \land I = f''I_0$$$

Lean4

@[simp]
theorem map_indep_iff {hf} {I : Set β} : (M.map f hf).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀ :=
  Iff.rfl

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