range_equiv_factorization — Mathlib

English

The natural factorization of the range equivalence respects the projection to LocallyConstant functions: composing the range equivalence with the first projection equals the map sending a point p to its value p.1 regarded as a LocallyConstant function.

Русский

Естественное факторизование эквивалентности образа совместимо с проекцией на локально константные функции: композиция range_equiv с первой проекцией равна отображению p ↦ p.1 как локально константная функция.

LaTeX

$$$\\big(\\operatorname{range\\_equiv}\\;C\\;ho\\;hsC\\big).toFun \\circ (\\text{first projection}) = (\\lambda p: p.1)^{\\operatorname{LocallyConstant}}$$$

Lean4

theorem range_equiv_factorization :
    (fun (p : ⋃ (e : { o' // o' < o }), (smaller C e.val)) ↦ p.1) ∘ (range_equiv C ho hsC).toFun =
      (fun (p : range C) ↦ (p.1 : LocallyConstant C ℤ)) :=
  rfl

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