hom_ext₁ — Mathlib

English

For ComposableArrows at level 1, two morphisms are equal if their components at positions 0 and 1 agree.

Русский

Для уровня 1 два морфизма равны, если их компоненты на позициях 0 и 1 совпадают.

LaTeX

$$$\forall {F,G : ComposableArrows\ C\ 1} {\phi \phi' : F ⟶ G},\ (app' \phi 0 = app' \phi' 0) \land (app' \phi 1 = app' \phi' 1) \Rightarrow \phi = \phi'$$$

Lean4

@[ext]
theorem hom_ext₁ {F G : ComposableArrows C 1} {φ φ' : F ⟶ G} (h₀ : app' φ 0 = app' φ' 0) (h₁ : app' φ 1 = app' φ' 1) :
    φ = φ' := by
  ext i
  match i with
  | 0 => exact h₀
  | 1 => exact h₁

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