mapEmbedding_indep_iff — Mathlib

English

If I is independent in M, then its image under the embedding f is independent in M.mapEmbedding f.

Русский

Если I независимо в M, то образ I под f независим в M.mapEmbedding f.

LaTeX

$$$M.Indep I \\rightarrow (M.mapEmbedding f).Indep (f '' I)$$$

Lean4

@[simp]
theorem mapEmbedding_indep_iff {f : α ↪ β} {I : Set β} : (M.mapEmbedding f).Indep I ↔ M.Indep (f ⁻¹' I) ∧ I ⊆ range f :=
  by
  rw [mapEmbedding, map_indep_iff]
  refine ⟨?_, fun ⟨h, h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
  rintro ⟨I, hI, rfl⟩
  rw [preimage_image_eq _ f.injective]
  exact ⟨hI, image_subset_range _ _⟩

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