partialTraj_le_def — Mathlib

English

For a ≤ b, the partial trajectory κ a b is obtained by iterating the kernels κ on successive steps from a to b, starting from the identity at a.

Русский

При a ≤ b частная траектория κ a b получается вычерчивая ядра κ на последовательно шагах от a до b, начиная с тождества в a.

LaTeX

$$partialTraj κ a b$$

Lean4

theorem partialTraj_le_def (hab : a ≤ b) :
    partialTraj κ a b =
      @Nat.leRec a (fun b _ ↦ Kernel (Π i : Iic a, X i) (Π i : Iic b, X i)) Kernel.id
        (fun k _ κ_k ↦ ((Kernel.id ×ₖ ((κ k).map (piSingleton k))) ∘ₖ κ_k).map (IicProdIoc k (k + 1))) b hab :=
  by
  obtain rfl | hab := eq_or_lt_of_le hab
  · simp
  · rw [partialTraj, dif_neg (not_le.2 hab)]

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