pi_ext' — Mathlib

English

An ext lemma for partially-applied ext: if for every i, f ∘ single_i = g ∘ single_i, then f=g.

Русский

Лемма ext для частично-applied ext: если для каждого i выполнено f ∘ single_i = g ∘ single_i, то f=g.

LaTeX

$$$\\forall i,\\; f\\circ (\\text{single}_i) = g\\circ (\\text{single}_i)\\Rightarrow f=g.$$$

Lean4

/-- This is used as the ext lemma instead of `LinearMap.pi_ext` for reasons explained in
note [partially-applied ext lemmas]. -/
@[ext]
theorem pi_ext' (h : ∀ i, f.comp (single R φ i) = g.comp (single R φ i)) : f = g :=
  by
  refine pi_ext fun i x => ?_
  convert LinearMap.congr_fun (h i) x

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