map_map — Mathlib

English

Applying f and then g to a subspace is the same as applying the composed map g ∘ f to the original subspace.

Русский

Применение отображений f затем g к подпроизвольству равно применению композиции g ∘ f к исходному подпроизвольству.

LaTeX

$$$ (s.map f).map g = s.map (g \\circ f)$$$

Lean4

theorem map_map (s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) : (s.map f).map g = s.map (g.comp f) :=
  coe_injective <| image_image _ _ _

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