coe_equivMapOfInjective_apply — Mathlib

English

Let s be a subring of R and f: R →+* S be injective. The forward map of the induced isomorphism between s and its image is the restriction of f to s; i.e., φ(x) = f(x) for all x ∈ s.

Русский

Пусть s — подкольцо R и f: R →+* S инъективен. Безусловно, отображение φ, задающее изоморфизм между s и его образом, совпадает с ограничением f на s: φ(x) = f(x) для всех x ∈ s.

LaTeX

$$$\\forall x\\in s,\\; \\phi(x) = f(x)$$$

Lean4

@[simp]
theorem coe_equivMapOfInjective_apply (f : R →+* S) (hf : Function.Injective f) (x : s) :
    (equivMapOfInjective s f hf x : S) = f x :=
  rfl

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