ofLEMk_comp_ofMkLEMk — Mathlib

English

The composition of two witnessing morphisms of MkLEMs is MkLEMk for the transitive inequality.

Русский

Сложение двух свидетельств mkLEMs даёт mkLEMk для переходного неравенства.

LaTeX

$$$\operatorname{ofMkLEMk} f g h_1 \;\circ\; \operatorname{ofMkLEMk} g h h_2 = \operatorname{ofMkLEMk} f h (h_1 \operatorname{trans} h_2)$$$

Lean4

@[reassoc (attr := simp)]
theorem ofLEMk_comp_ofMkLEMk {B A₁ A₂ : C} (X : Subobject B) (f : A₁ ⟶ B) [Mono f] (g : A₂ ⟶ B) [Mono g] (h₁ : X ≤ mk f)
    (h₂ : mk f ≤ mk g) : ofLEMk X f h₁ ≫ ofMkLEMk f g h₂ = ofLEMk X g (h₁.trans h₂) :=
  by
  simp only [ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc, Iso.hom_inv_id_assoc]
  congr 1

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