mapSetEquiv_indep_iff — Mathlib

English

For a matroid M on α and an equivalence e: M.E ≃ E, a set I of β is independent in the transported matroid M.mapSetEquiv e if and only if its preimage under e (applied to E ∩ I) is independent in M and I ⊆ E.

Русский

Пусть M — матроид на α и e: M.E ≃ E — эквивалентность. Набор I ⊆ E независим в переносном матроиде M.mapSetEquiv e тогда и только тогда, когда его образный предобраз через e по E ∩ I является независимым в M и I ⊆ E.

LaTeX

$$$(M.mapSetEquiv\, e).Indep(I) \\iff M.Indep\\bigl(e^{-1}(E \\cap I)\\bigr) \\wedge I \\subseteq E$$$

Lean4

@[simp]
theorem mapSetEquiv_indep_iff (M : Matroid α) {E : Set β} (e : M.E ≃ E) {I : Set β} :
    (M.mapSetEquiv e).Indep I ↔ M.Indep ↑(e.symm '' (E ↓∩ I)) ∧ I ⊆ E :=
  Iff.rfl

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