isEmbedding_hom — Mathlib

English

The map f ↦ f.hom from Hom(A, R) to the set of functions A → R is an embedding; i.e., it is injective and its topology is induced from the product topology on R^A.

Русский

Отображение f ↦ f.hom из множества гомоморфизмов в R в множество функций A → R является вложением: оно инъективно, топология индуцирована произведением R^A.

LaTeX

$$$\text{IsEmbedding}\big(\lambda f: A \to R. f\text{.hom}\big)$$$

Lean4

theorem isEmbedding_hom : IsEmbedding (fun f : A ⟶ R ↦ (f.hom : A → R)) :=
  ⟨.induced _, fun _ _ e ↦ by ext; rw [e]⟩

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