ext — Mathlib

English

The extensional equivalence for weights asserts that if two weights χ1, χ2 agree pointwise on L, then they are equal as Weight objects.

Русский

Экстенциальное равенство весов: если χ1(x) = χ2(x) для всех x ∈ L, то χ1 = χ2 как объекты веса.

LaTeX

$$$\\forall x\\in L, χ_1(x) = χ_2(x) \\Rightarrow χ_1 = χ_2$$$

Lean4

@[ext]
theorem ext {χ₁ χ₂ : Weight R L M} (h : ∀ x, χ₁ x = χ₂ x) : χ₁ = χ₂ := by obtain ⟨f₁, _⟩ := χ₁; obtain ⟨f₂, _⟩ := χ₂;
  aesop

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