comp_map — Mathlib

English

Applying the map to a composition equals composing the maps: map_{F}(g ∘ f) x = map_{F}(g)(map_{F}(f) x).

Русский

Применение отображения к композиции равно композиции отображений: F.map(g ∘ f) x = F.map g (F.map f x).

LaTeX

$$$$q.map(\\circ\\, g\\, f)\\,x = q.map\\, g\\,(q.map\\, f\\,x).$$$$

Lean4

@[simp]
theorem comp_map {α β γ : TypeVec n} (f : α ⟹ β) (g : β ⟹ γ) (x : F α) : (g ⊚ f) <$$> x = g <$$> f <$$> x :=
  by
  rw [← abs_repr x, ← abs_map, ← abs_map, ← abs_map]
  rfl

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