partialTraj_succ_of_le — Mathlib

English

If a ≤ b, then partialTraj κ a (b+1) equals the composition of the previous trajectory with κ b, mapped by IicProdIoc(b,b+1).

Русский

Если a ≤ b, то partialTraj κ a (b+1) равен композиции предыдущей траектории с κ b, отображенной через IicProdIoc(b,b+1).

LaTeX

$$partialTraj κ a (b+1)$$

Lean4

theorem partialTraj_succ_of_le (hab : a ≤ b) :
    partialTraj κ a (b + 1) =
      ((Kernel.id ×ₖ ((κ b).map (piSingleton b))) ∘ₖ partialTraj κ a b).map (IicProdIoc b (b + 1)) :=
  by
  rw [partialTraj, dif_neg (by cutsat)]
  induction b, hab using Nat.le_induction with
  | base => simp
  | succ k hak hk => rw [Nat.leRec_succ, ← partialTraj_le_def]; cutsat

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