ext — Mathlib

English

Two families of elements on a presieve are equal if they coincide on every arrow; extensionality principle.

Русский

Две совокупности элементов на презиве равны, если они совпадают на каждом стрелке; принцип экстенсиональности.

LaTeX

$$$\\forall x,y:\\; R.FamilyOfElements\\; P,\\; (\\forall Y,f,hf:\\; R(f),\\; x(f,hf)=y(f,hf)) \\Rightarrow x=y$$$

Lean4

@[ext]
theorem ext {R : Presieve X} {x y : R.FamilyOfElements P} (H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf) :
    x = y := by
  funext Z f hf
  exact H f hf

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