mapSetEmbedding_indep_iff — Mathlib

English

Independence in the embedded matroid is characterized by independence of the preimage and inclusion in the range.

Русский

Независимость после внедрения определяется независимостью предобраза и включением в образ.

LaTeX

$$$ (M.mapSetEmbedding f).Indep I \iff M.Indep (f^{-1}(I)) \land I \subseteq \mathrm{range}(f) $$$

Lean4

@[simp]
theorem mapSetEmbedding_indep_iff {f : M.E ↪ β} {I : Set β} :
    (M.mapSetEmbedding f).Indep I ↔ M.Indep ↑(f ⁻¹' I) ∧ I ⊆ range f :=
  Iff.rfl

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