mapEquiv_indep_iff — Mathlib

English

IsBasis for a mapped matroid corresponds to IsBasis' on the original after applying f.symm to I and X.

Русский

IsBasis для отображённого матроида соответствует IsBasis' для исходного после применения f.symm к I и X.

LaTeX

$$$(M.mapEquiv f).IsBasis I X \iff M.IsBasis (f.symm '' I) (f.symm '' X)$$$

Lean4

@[simp]
theorem mapEquiv_indep_iff {I : Set β} : (M.mapEquiv f).Indep I ↔ M.Indep (f.symm '' I) :=
  by
  rw [mapEquiv_eq_map, map_indep_iff]
  exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

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