mapSetEmbedding_indep_iff' — Mathlib

English

Same as the previous statement, expressing the existence of a preimage I0 with I = f''I0.

Русский

То же самое утверждение: существует I0 с I = f''I0.

LaTeX

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

Lean4

theorem mapSetEmbedding_indep_iff' {f : M.E ↪ β} {I : Set β} :
    (M.mapSetEmbedding f).Indep I ↔ ∃ (I₀ : Set M.E), M.Indep ↑I₀ ∧ I = f '' I₀ :=
  by
  simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
  constructor
  · rintro ⟨hI, I, rfl⟩
    exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩
  rintro ⟨I, hI, rfl⟩
  rw [preimage_image_eq _ f.injective]
  exact ⟨hI, _, rfl⟩

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