exists_eq_image_of_mapSetEmbedding

English

If I is independent in M.mapSetEmbedding f, then there exists I0 ⊆ M.E such that I = f''I0 and I0 is independent in M.

Русский

Если I независимо в M.mapSetEmbedding f, то существует I0 ⊆ M.E such that I = f''I0 и I0 независимо в M.

LaTeX

$$$\exists I_0 \subseteq M.E,\ M.Indep I_0 \land I = f''I_0$$$

Lean4

theorem exists_eq_image_of_mapSetEmbedding {f : M.E ↪ β} {I : Set β} (hI : (M.mapSetEmbedding f).Indep I) :
    ∃ (I₀ : Set M.E), M.Indep I₀ ∧ I = f '' I₀ :=
  ⟨f ⁻¹' I, hI.1, Eq.symm <| image_preimage_eq_of_subset hI.2⟩

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