comp — Mathlib

English

If g is injective on t, f is injective on s, and MapsTo f s t, then g ∘ f is injective on s.

Русский

Если g инъективна на t, f инъективна на s, и f отображает s в t, то g ∘ f инъективна на s.

LaTeX

$$$ (\\operatorname{InjOn} g t) \\land (\\operatorname{InjOn} f s) \\land (\\operatorname{MapsTo} f s t) \\Rightarrow \\operatorname{InjOn}(g \\circ f) s$$

Lean4

theorem comp (hg : InjOn g t) (hf : InjOn f s) (h : MapsTo f s t) : InjOn (g ∘ f) s := fun _ hx _ hy heq =>
  hf hx hy <| hg (h hx) (h hy) heq

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