comp — Mathlib

English

If f lifts φ and g lifts ψ, then f ≫ g lifts φ ≫ ψ.

Русский

Если f поднимает φ, а g поднимает ψ, то композиция f ≫ g поднимает композицию φ ≫ ψ.

LaTeX

$$$$ p.IsHomLift f \; \varphi \quad \text{ и } \quad p.IsHomLift g \; \psi \quad \Rightarrow \quad p.IsHomLift (f \gg g) \; (\varphi \gg \psi) $$$$

Lean4

instance comp {R S T : 𝒮} {a b c : 𝒳} (f : R ⟶ S) (g : S ⟶ T) (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift f φ]
    [p.IsHomLift g ψ] : p.IsHomLift (f ≫ g) (φ ≫ ψ) :=
  by
  apply of_commSq
  on_goal 1 => rw [p.map_comp]
  apply CommSq.horiz_comp (commSq p f φ) (commSq p g ψ)

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