isReflexivePair — Mathlib

English

If f,g form a kernel pair for some q, then the pair f,g is reflexive.

Русский

Если f,g образуют пару ядра для некоторого q, то эта пара рефлексивна.

LaTeX

$$$\text{If } \mathsf{IsKernelPair}(q,f,g) \Rightarrow \text{IsReflexivePair}(f,g)$$$

Lean4

/-- If `f,g` is a kernel pair for some morphism `q`, then it is reflexive. -/
theorem isReflexivePair {R : C} {f g : R ⟶ A} {q : A ⟶ B} (h : IsKernelPair q f g) : IsReflexivePair f g :=
  IsReflexivePair.mk' _ (h.lift' _ _ rfl).2.1
    (h.lift' _ _ _).2.2
      -- This shouldn't be an instance as it would instantly loop.

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