smul_graphOn_univ — Mathlib

English

Special case of the previous result with s = univ: the image under x of the whole graph of f is the graph of a transformed function on the entire domain.

Русский

Особый случай предыдущего результата, где S = все пространство: образ графика f под действием x равен графику преобразованной функции на всей области определения.

LaTeX

$$$x \\cdot \\mathrm{graphOn}(f,\\mathrm{univ}) = \\mathrm{graphOn}(a,b \\mapsto (x_2 / f(x_1)) \\cdot f(a))$$$

Lean4

@[to_additive]
theorem smul_graphOn_univ (x : α × β) (f : F) : x • univ.graphOn f = univ.graphOn fun a ↦ x.2 / f x.1 * f a := by
  simp [smul_graphOn]

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