infTo_commutes — Mathlib

English

For any X,Y ∈ O and f: X ⟶ Y in H, the relation infTo mX ≫ f = infTo mY holds.

Русский

Для любых X,Y ∈ O и f: X → Y из H выполняется infTo mX ≫ f = infTo mY.

LaTeX

$$$\forall X,Y\in O, \forall f: X\to Y, mf \Rightarrow \infTo(mX) \;\!\!\!\!\!\!\!\! \!\!\! \; f = \infTo(mY)$$$

Lean4

/-- The triangles consisting of a morphism in `H` and the maps from `inf O H` commute.
-/
theorem infTo_commutes {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}
    (mf : (⟨X, Y, mX, mY, f⟩ : Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H) : infTo O H mX ≫ f = infTo O H mY :=
  (inf_exists O H).choose_spec.choose_spec mX mY mf

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