comp_left — Mathlib

English

If f is locally injective and g is injective, then f ∘ g is locally injective.

Русский

Если f локально инъективна и g инъективна, то композиция f ∘ g локально инъективна.

LaTeX

$$IsLocallyInjective f \rightarrow IsLocallyInjective (f ∘ g)$$

Lean4

theorem comp_left {A} {f : X → Y} (hf : IsLocallyInjective f) {g : Y → A} (hg : g.Injective) :
    IsLocallyInjective (g ∘ f) := fun x ↦
  let ⟨U, hU, hx, inj⟩ := hf x;
  ⟨U, hU, hx, hg.comp_injOn inj⟩

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