separatesPoints_charPoly — Mathlib

English

The family {char he hL w} separates points of V: for distinct v,v' in V there exists w with char he hL w v ≠ char he hL w v'.

Русский

Семейство функций-символов разделяет точки: для различных v,v' ∈ V найдётся w, такое что χ_w(v) ≠ χ_w(v').

LaTeX

$$$\\text{There exist } w \\in W \\text{ with } (v \\mapsto e(L(v,w))) \\neq (v' \\mapsto e(L(v',w))).$$$

Lean4

/-- The family `charPoly he hL w, w : W` separates points in `V`. -/
theorem separatesPoints_charPoly (he : Continuous e) (he' : e ≠ 1) (hL : Continuous fun p : V × W ↦ L p.1 p.2)
    (hL' : ∀ v ≠ 0, L v ≠ 0) : ((charPoly he hL).map (toContinuousMapStarₐ ℂ)).SeparatesPoints :=
  by
  intro v v' hvv'
  obtain ⟨w, hw⟩ : ∃ w, char he hL w v ≠ char he hL w v' :=
    by
    contrapose! hvv'
    exact ext_of_char_eq he he' hL hL' hvv'
  use char he hL w
  simp only [StarSubalgebra.coe_toSubalgebra, StarSubalgebra.coe_map, Set.mem_image, SetLike.mem_coe,
    exists_exists_and_eq_and, ne_eq]
  exact ⟨⟨char he hL w, char_mem_charPoly w, rfl⟩, hw⟩

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