range_comp' — Mathlib

English

Variant of Range Composition: range (fun x => g (f x)) = g '' range f.

Русский

Вариант выражения для композиции: range (lambda x, g (f x)) = g '' range f.

LaTeX

$$$ \\operatorname{range}\$\\lambda x. g(f(x))\$ = g''\\operatorname{range} f$$$

Lean4

/-- Variant of `range_comp` using a lambda instead of function composition.
-/
theorem range_comp' (g : α → β) (f : ι → α) : range (fun x => g (f x)) = g '' range f :=
  range_comp g f

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