comp_apply — Mathlib

English

Let f be a bounded continuous map α → β and G: β → γ be Lipschitz with constant C. Then the target-composed map a ↦ G(f(a)) is the value of (f.comp G H) at a.

Русский

Пусть f: α →ᵇ β — ограниченно непрерывное отображение, G: β → γ — Lipschitz с константой C. Тогда (f.comp G H) принимает значение G(f(a)) в точке a.

LaTeX

$$$(f\\text{.comp } G\\ H)\\,a = G(f(a))$$$

Lean4

@[simp]
theorem comp_apply (G : β → γ) {C : ℝ≥0} (H : LipschitzWith C G) (f : α →ᵇ β) (a : α) : (f.comp G H) a = G (f a) :=
  rfl

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