traj_map_frestrictLe — Mathlib

English

For all a,b, (traj κ a).map (frestrictLe b) equals partialTraj κ a b.

Русский

Для всех a,b: (traj κ a).map (frestrictLe b) = partialTraj κ a b.

LaTeX

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

Lean4

theorem traj_map_frestrictLe (a b : ℕ) : (traj κ a).map (frestrictLe b) = partialTraj κ a b :=
  by
  ext x
  rw [map_apply, traj_apply, frestrictLe, isProjectiveLimit_trajFun, inducedFamily_Iic]
  fun_prop

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