map_span — Mathlib

English

The affine span of a set is mapped to the affine span of its image.

Русский

Афинный замыкание множества отображается в афинное замыкание его изображения.

LaTeX

$$$ (\\\\mathrm{affineSpan} \\\\ k \\\\ s).map f = affineSpan \\\\ k (f \\\\ '' \\\\ s)$$$

Lean4

theorem map_span (s : Set P₁) : (affineSpan k s).map f = affineSpan k (f '' s) :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
  · simp
  apply ext_of_direction_eq
  · simp [direction_affineSpan]
  · exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp), subset_affineSpan k _ (mem_image_of_mem f hp)⟩

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