instFunLike — Mathlib

English

An extensional principle for weights: two weights are equal if they have identical evaluation on every x ∈ L. This yields an extensionality lemma for Weight objects.

Русский

Принцип экстентальности весов: два веса равны, если для каждого x ∈ L они дают одинаковые значения; это даёт лемму экстентности для объектов веса.

LaTeX

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

Lean4

instance instFunLike : FunLike (Weight R L M) L R where
  coe χ := χ.1
  coe_injective' χ₁ χ₂ h := by cases χ₁; cases χ₂; simp_all

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