English
Two incidence-algebra elements are equal if they agree on all comparable pairs.
Русский
Два элемента инцидентной алгебры равны, если их значения совпадают на всех сравнимых парах (a ≤ b).
LaTeX
$$∀ f g : IncidenceAlgebra 𝕜 α, (∀ a b, a ≤ b → f a b = g a b) → f = g$$
Lean4
@[ext]
theorem ext ⦃f g : IncidenceAlgebra 𝕜 α⦄ (h : ∀ a b, a ≤ b → f a b = g a b) : f = g :=
by
refine DFunLike.coe_injective' (funext₂ fun a b ↦ ?_)
by_cases hab : a ≤ b
· exact h _ _ hab
· rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]