pre_map — Mathlib

English

Pre-map distributes over composition: pre (f ≫ g) = pre g ≫ pre f.

Русский

Pre-мэп распределяется по композиции: pre (f ≫ g) = pre g ≫ pre f.

LaTeX

$$$\mathrm{pre}(f \circ g) = \mathrm{pre}(g) \circ \mathrm{pre}(f)$$$

Lean4

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

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