ext — Mathlib

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]

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