pre_map — Mathlib

English

For exponentiable A1,A2,A3 and morphisms f: A1 ⟶ A2, g: A2 ⟶ A3, we have pre (f ≫ g) = pre g ≫ pre f.

Русский

Пусть A1,A2,A3 экспоненцируемы и f:A1⟶A2, g:A2⟶A3. Тогда pre (f ≫ g) = pre g ≫ pre f.

LaTeX

$$$ {A_1 A_2 A_3 : C} \; [Exponentiable A_1] [Exponentiable A_2] [Exponentiable A_3] (f : A_1 ⟶ A_2) (g : A_2 ⟶ A_3) :\n \operatorname{pre} (f \circ g) = \operatorname{pre} g \circ \operatorname{pre} f$$$

Lean4

@[simp]
theorem pre_map {A₁ A₂ A₃ : C} [Exponentiable A₁] [Exponentiable A₂] [Exponentiable A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
    pre (f ≫ g) = pre g ≫ pre f := by
  rw [pre, pre, pre, conjugateEquiv_comp]
  simp

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