traj_map_frestrictLe_apply — Mathlib

English

(traj κ a x).map (frestrictLe b) = partialTraj κ a b x for all a,b and x.

Русский

(traj κ a x).map (frestrictLe b) = partialTraj κ a b x для всех a,b и x.

LaTeX

$$$\\forall a,b,x:\\ (traj\\ κ\\ a\\ x).map (frestrictLe\\ b) = partialTraj\\ κ\\ a\\ b\\ x$$$

Lean4

theorem traj_map_frestrictLe_apply (a b : ℕ) (x : Π i : Iic a, X i) :
    (traj κ a x).map (frestrictLe b) = partialTraj κ a b x := by
  rw [← map_apply _ (measurable_frestrictLe b), traj_map_frestrictLe]

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