map_map — Mathlib

English

Mapping first by f and then by g equals mapping by the composition g ∘ f: (E.map f).map g = E.map (g.comp f).

Русский

Послойное отображение: отображение сначала f, затем g эквивалентно отображению через композицию g ∘ f.

LaTeX

$$$ (E.map f).map g = E.map (g.comp f) $$$

Lean4

theorem map_map {K L₁ L₂ L₃ : Type*} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂] [Field L₃]
    [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
    (E.map f).map g = E.map (g.comp f) :=
  SetLike.coe_injective <| Set.image_image _ _ _

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