map_image_indep_iff — Mathlib

English

If I is a subset of M.E, then the mapped independence of I equals the independence of I in M.

Русский

Если I ⊆ M.E, то независимость образа I в отображенном матроиде эквивалентна независимости I в M.

LaTeX

$$$\text{If } I \subseteq M.E:\ (M.map f hf).Indep (f(I)) \iff M.Indep I$$$

Lean4

theorem map_image_indep_iff {hf} {I : Set α} (hI : I ⊆ M.E) : (M.map f hf).Indep (f '' I) ↔ M.Indep I :=
  by
  rw [map_indep_iff]
  refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩⟩
  rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ; rwa [hIJ]

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