mapEmbedding_isBase_iff — Mathlib

English

For an embedding f, the mapped base status on B is equivalent to the base status on the preimage plus the subset relations B ⊆ range f.

Русский

Для вложения f статус базы для отображаемого множества равносилен статусу базы для предобраза плюс отношения подмножества B ⊆ range f.

LaTeX

$$$(M.mapEmbedding f).IsBase B \\iff M.IsBase (f^{-1}' B) \\wedge B \\subseteq \\operatorname{range} f$$$

Lean4

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

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