Translating functions

def Function.translate {G : Type u_1} {α : Type u_2} [Group G] (x : G) (f : G → α) : G → α

Left-translation of a function: τ_[x] f y := f (x⁻¹ * y).

Equations

• τ_[x] f y = f (x⁻¹ * y)

def Function.«termτ_[_]» : Lean.ParserDescr

Left-translation of a function: τ_[x] f y := f (x⁻¹ * y).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Function.translate_apply {G : Type u_1} {α : Type u_2} [Group G] (x : G) (f : G → α) (y : G) : τ_[x] f y = f (x⁻¹ * y)

@[simp]

theorem Function.translate_one {G : Type u_1} {α : Type u_2} [Group G] (f : G → α) : τ_[1] f = f

@[simp]

theorem Function.translate_translate {G : Type u_1} {α : Type u_2} [Group G] (x y : G) (f : G → α) : τ_[x] (τ_[y] f) = τ_[x * y] f

@[simp]

theorem Function.translate_const {G : Type u_1} {α : Type u_2} [Group G] (x : G) (a : α) : τ_[x] (const G a) = const G a

@[simp]

theorem Function.translate_fun_const {G : Type u_1} {α : Type u_2} [Group G] (x : G) (a : α) : (τ_[x] fun (x : G) => a) = fun (x : G) => a

Eta-expanded form of Function.translate_const

@[simp]

theorem Function.translate_one_fun {G : Type u_1} {M : Type u_3} [Group G] [One M] (x : G) : τ_[x] 1 = 1

@[simp]

theorem Function.translate_zero_fun {G : Type u_1} {M : Type u_3} [Group G] [Zero M] (x : G) : τ_[x] 0 = 0

@[simp]

theorem Function.translate_mul_fun {G : Type u_1} {M : Type u_3} [Group G] [Mul M] (x : G) (f g : G → M) : τ_[x] (f * g) = τ_[x] f * τ_[x] g

@[simp]

theorem Function.translate_add_fun {G : Type u_1} {M : Type u_3} [Group G] [Add M] (x : G) (f g : G → M) : τ_[x] (f + g) = τ_[x] f + τ_[x] g

@[simp]

theorem Function.range_translate {G : Type u_1} {α : Type u_2} [Group G] (x : G) (f : G → α) : Set.range (τ_[x] f) = Set.range f

@[simp]

theorem Bornology.isBddFun_translate {G : Type u_1} {X : Type u_2} [Group G] [Bornology X] {x : G} {f : G → X} : IsBddFun (τ_[x] f) ↔ IsBddFun f

theorem Bornology.IsBddFun.translate {G : Type u_1} {X : Type u_2} [Group G] [Bornology X] {x : G} {f : G → X} : IsBddFun f → IsBddFun (τ_[x] f)

Alias of the reverse direction of Bornology.isBddFun_translate.