map_span — Mathlib

English

The span under a map of a span equals the span of the image set (alternative formulation).

Русский

Порождение образа под отображением эквивалентно порождению образа множества.

LaTeX

$$$ map f (span s) = span (f '' s) $$$

Lean4

theorem map_span (f : F) (s : Set R) : map f (span s) = span (f '' s) :=
  by
  refine (Submodule.span_eq_of_le _ ?_ ?_).symm
  · rintro _ ⟨x, hx, rfl⟩; exact mem_map_of_mem f (subset_span hx)
  · rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]
    exact subset_span

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