def LeanSubst.Subst.map {A : Type u_1} {B : Type u_2} (f : A → B) : Subst A → Subst B

Equations

• LeanSubst.Subst.map f x✝¹ x✝ = match x✝¹ x✝ with | LeanSubst.Subst.Action.su t => LeanSubst.Subst.Action.su (f t) | LeanSubst.Subst.Action.re k => LeanSubst.Subst.Action.re k

@[simp]

theorem LeanSubst.Subst.map_rename_seq {A : Type u} {B : Type v} {f : A → B} {k : Nat} {σ : Subst A} : map f (#k::σ) = #k::map f σ

@[simp]

theorem LeanSubst.Subst.map_replace_seq {A : Type u} {B : Type v} {f : A → B} {t : A} {σ : Subst A} : map f (%t::σ) = %(f t)::map f σ

@[simp]

theorem LeanSubst.Subst.map_rename_noop {A : Type u} {B : Type v} {f : A → B} {r : Ren} : map f r.to = r.to

@[simp]

theorem LeanSubst.Subst.map_I_noop {A : Type u} {B : Type v} {f : A → B} : map f I = I

@[simp]

theorem LeanSubst.Subst.map_S_noop {A : Type u} {B : Type v} {f : A → B} : map f S = S

theorem LeanSubst.Subst.map_rename_compose_left {A : Type u} {B : Type v} {τ : Subst A} [SubstMap A] [SubstMap B] {f : A → B} {r : Ren} : (∀ (t : A), f (t[r.to]) = f t[r.to]) → map f (τ ∘ r.to) = map f τ ∘ r.to

@[simp]

theorem LeanSubst.Subst.map_rename_compose_right {A : Type u} {B : Type v} {σ : Subst A} [SubstMap A] [SubstMap B] {f : A → B} {r : Ren} : map f (r.to ∘ σ) = r.to ∘ map f σ

theorem LeanSubst.Subst.map_S_compose_left {A : Type u} {B : Type v} {τ : Subst A} [SubstMap A] [SubstMap B] {f : A → B} : (∀ (t : A), f (t[S]) = f t[S]) → map f (τ ∘ S) = map f τ ∘ S

@[simp]

theorem LeanSubst.Subst.map_S_compose_right {A : Type u} {B : Type v} {σ : Subst A} [SubstMap A] [SubstMap B] {f : A → B} : map f (S ∘ σ) = S ∘ map f σ