coe_injective — Mathlib

English

Let α be nontrivial. The map sending a line to its toFun function is injective: if l.toFun = m.toFun then l = m.

Русский

Пусть α ненулевой. Отображение линии к её функции toFun инъективно: если l.toFun = m.toFun, то l = m.

LaTeX

$$$[Nontrivial\\ α] \\Rightarrow \\forall l,m : Line\\, α\\,\\iota,\\ l.toFun = m.toFun \\Rightarrow l = m.$$$

Lean4

theorem coe_injective [Nontrivial α] : Injective ((⇑) : Line α ι → α → ι → α) :=
  by
  rintro l m hlm
  ext i a
  obtain ⟨b, hba⟩ := exists_ne a
  simp only [funext_iff] at hlm ⊢
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · cases hi : idxFun m i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i
  · cases hi : idxFun l i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i

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