comp_left — Mathlib

English

Composition on the left by an injective function yields an injective map on function spaces.

Русский

Слева композиция накладывается инъективной функцией и порождает инъективное отображение между пространствами функций.

LaTeX

$$$Injective\\,g \\rightarrow Injective\\,(g \\circ \\cdot)$$$

Lean4

/-- Composition by an injective function on the left is itself injective. -/
theorem comp_left {g : β → γ} (hg : Injective g) : Injective (g ∘ · : (α → β) → α → γ) :=
  .piMap fun _ ↦ hg

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