extend_injective — Mathlib

English

If f is injective, then the map g ↦ extend f g e' is injective.

Русский

Если f инъективна, то отображение g ↦ extend f g e' инъективно.

LaTeX

$$$\operatorname{Injective}(f) \rightarrow \operatorname{Injective}(\lambda g, \operatorname{extend} f g e')$$$

Lean4

theorem extend_injective (hf : Injective f) (e' : β → γ) : Injective fun g ↦ extend f g e' :=
  by
  intro g₁ g₂ hg
  refine funext fun x ↦ ?_
  have H := congr_fun hg (f x)
  simp only [hf.extend_apply] at H
  exact H

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