ext — Mathlib

English

Extensionality principle for MonObj: equality of multiplication implies equality of objects.

Русский

Принцип экстенсиональности для MonObj: равенство умножений влечёт равенство объектов.

LaTeX

$$$\\text{MonObj.ext}$$$

Lean4

@[ext]
theorem ext {X : C} (h₁ h₂ : MonObj X) (H : h₁.mul = h₂.mul) : h₁ = h₂ :=
  by
  suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl
  trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul
  · simp [tensorHom_def, H, ← unitors_equal]
  · simp [tensorHom_def']

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