ext — Mathlib

English

Extensionality for the second object in the equalizer sieve; equality follows from pointwise equal projections.

Русский

Экстенсиональность для второго объекта в сито равновесного конструирования; равенство следует из покомпонентного равенства проекций.

LaTeX

$$$$ \text{ext}(z_1,z_2) \Rightarrow z_1 = z_2 $$$$

Lean4

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

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