traj_map_frestrictLe_of_le — Mathlib

English

If a ≤ b, then (traj κ b).map (frestrictLe a) equals the deterministic kernel with the restriction frestrictLe₂ hab and measurability given by measurable_frestrictLe₂.

Русский

Если a ≤ b, то (traj κ b).map (frestrictLe a) равно детерминированному ядру с ограничением frestrictLe₂ hab и измеримостью given by measurable_frestrictLe₂.

LaTeX

$$$\\forall (hab : a \\le b),\\ (traj\\ κ\\ b).map (frestrictLe\\ a) = deterministic (frestrictLe₂\\ hab) (measurable_frestrictLe₂\\ _)$$$

Lean4

theorem traj_map_frestrictLe_of_le {a b : ℕ} (hab : a ≤ b) :
    (traj κ b).map (frestrictLe a) = deterministic (frestrictLe₂ hab) (measurable_frestrictLe₂ _) := by
  rw [traj_map_frestrictLe, partialTraj_le]

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