ext — Mathlib

English

Elements of the equalizer first object are determined by their projections; equality is extensional.

Русский

Элементы первого объекта равносильности определяются проекциями; равенство экстенсионально.

LaTeX

$$$$ (z_1 = z_2) \iff (\forall Y,f, hf, \; \Pi.\pi(\langle Y,f,hf \rangle) z_1 = \Pi.\pi(\langle Y,f,hf \rangle) z_2) $$$$

Lean4

@[ext]
theorem ext (z₁ z₂ : FirstObj P R)
    (h :
      ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
        (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₁ = (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₂) :
    z₁ = z₂ := by
  apply Limits.Types.limit_ext
  rintro ⟨⟨Y, f, hf⟩⟩
  exact h Y f hf

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