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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LeanSubst.Subst.map_I_noop {A B : Type} {f : A → B} : map f +0 = +0

@[simp]

theorem LeanSubst.Subst.map_S_noop {A B : Type} {f : A → B} : map f +1 = +1

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

@[simp]

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

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

@[simp]

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