English
Let f: Fin(n+1) →o Fin(m+1) and g: Fin(m+1) →o Fin(p+1) be order-preserving. Then map' respects composition: map'(f)(map'(g)(x)) = map'(g∘f)(x) for all x.
Русский
Пусть f: Fin(n+1) →o Fin(m+1) и g: Fin(m+1) →o Fin(p+1) — упорядоченные отображения. Тогда map' сохраняет композицию: map'(f)(map'(g)(x)) = map'(g∘f)(x) для всех x.
LaTeX
$$$map'(f)(map'(g)(x)) = map'(g\\circ f)(x)$$$
Lean4
theorem map'_map' {p : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (g : Fin (m + 1) →o Fin (p + 1)) (x : Fin (p + 2)) :
map' f (map' g x) = map' (g.comp f) x :=
by
obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
· obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
· rw [hy]
rw [map'_eq_castSucc_iff] at hy
obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
· rw [hz, Eq.comm]
rw [map'_eq_castSucc_iff] at hz ⊢
constructor
· refine hy.1.trans ?_
simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
exact g.monotone (by simpa using hz.1)
· intro i hi
exact hy.2 (f i) (by simpa using hz.2 i hi)
· rw [hz, Eq.comm]
rw [map'_eq_last_iff] at hz ⊢
intro i
exact hy.2 (f i) (by simpa using hz i)
· rw [Eq.comm, hx, map'_last]
rw [map'_eq_last_iff] at hx ⊢
intro i
apply hx
· simp
