mapEquiv_isBasis_iff — Mathlib

English

If M is rank-finite, then M.mapEquiv f is rank-finite.

Русский

Если M имеет конечный ранг, то M.mapEquiv f имеет конечный ранг.

LaTeX

$$$\operatorname{RankFinite}(M) \Rightarrow \operatorname{RankFinite}(M.mapEquiv f)$$$

Lean4

@[simp]
theorem mapEquiv_isBasis_iff {α β : Type*} {M : Matroid α} (f : α ≃ β) {I X : Set β} :
    (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (f.symm '' I) (f.symm '' X) :=
  by
  rw [mapEquiv_eq_map, map_isBasis_iff']
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨_, _, h, by simp, by simp⟩⟩
  obtain ⟨I, X, hIX, rfl, rfl⟩ := h
  simpa

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