range_equiv_smaller — Mathlib

English

There is an equivalence between the range of GoodProducts and the smaller set.

Русский

Существует эквивалентность между диапазоном GoodProducts и меньшим множеством.

LaTeX

$$$$\\text{Equiv}\\; (\\mathrm{range}\\; (\\mathrm{π}\\; C)) \\; (\\mathrm{smaller})$$$$

Lean4

/-- The equivalence from the image of the `GoodProducts` in `LocallyConstant (π C (ord I · < o)) ℤ` to
`smaller C o`
-/
noncomputable def range_equiv_smaller (o : Ordinal) : range (π C (ord I · < o)) ≃ smaller C o :=
  Equiv.ofBijective (range_equiv_smaller_toFun C o) (range_equiv_smaller_toFun_bijective C o)

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