English
Let η, α, ι be types with α nontrivial. Two subspaces l, m of η → α indexed by ι are equal whenever their evaluation maps agree on all inputs, i.e. for every x: η → α and every i ∈ ι, l x i = m x i.
Русский
Пусть η, α, ι – множества, α не тривиально. Два подпространства l и m подпространства η → α, индексируемые ι, равны, если их отображения-в-значения согласуются на всех входах: для каждого x: η → α и каждого i ∈ ι выполняется l x i = m x i.
LaTeX
$$$[Nontrivial\\ α] \\Rightarrow \\forall l,m : Subspace\\,\\eta\\,\\alpha\\,\\iota,\\ (l.toFun = m.toFun) \\Rightarrow l = m, \\text{ where } (l.toFun)(x,i) = l\\,x\\,i.$$$
Lean4
theorem coe_injective [Nontrivial α] : Injective ((⇑) : Subspace η α ι → (η → α) → ι → α) := by
classical
rintro l m hlm
ext i
simp only [funext_iff] at hlm
cases hl : idxFun l i with
| inl a =>
obtain ⟨b, hba⟩ := exists_ne a
cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
| inr e =>
cases hm : idxFun m i with
| inl a =>
obtain ⟨b, hba⟩ := exists_ne a
simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
| inr f =>
obtain ⟨a, b, hab⟩ := exists_pair_ne α
simp only [Sum.inr.injEq]
by_contra! hef
simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i
