English
For x ∈ α × β, a subset s ⊆ α, and a function f in F, the image of the graph of f over s under the action by x equals the graph of a transformed function g over the translated set x.1 • s, where g(t) = (x.2 / f(x.1)) · f(t).
Русский
Для x = (a,b) и подмножества S ⊆ α и функции f, изображение графика f над S под действием x равно графику новой функции g над преобразованным множеством a • S, где g(t) = (b / f(a)) · f(t).
LaTeX
$$$\\forall x=(x_1,x_2),\\ s\\subseteq \\alpha,\\ f\\in F:\\ x·\\mathrm{graphOn}(f,s) = \\mathrm{graphOn}(\\lambda a.\\ x_2 / f(x_1) \\cdot f(a))\\\\ \\text{on } x_1 \\cdot s$$$
Lean4
@[to_additive]
theorem smul_graphOn (x : α × β) (s : Set α) (f : F) : x • s.graphOn f = (x.1 • s).graphOn fun a ↦ x.2 / f x.1 * f a :=
by
ext ⟨a, b⟩
simp [mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul, mul_left_comm _ _⁻¹, eq_inv_mul_iff_mul_eq,
← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]
