equiv_range — Mathlib

English

There is an equivalence between GoodProducts and its range: GoodProducts ≃ range C.

Русский

Существует эквиваленция между GoodProducts и его образом: GoodProducts ≃ range C.

LaTeX

$$$$ \\mathrm{equiv\\_range}(C) : \\mathrm{GoodProducts}\\, C \\simeq \\mathrm{range}\\, C. $$$$

Lean4

/-- The type of good products is equivalent to its image. -/
noncomputable def equiv_range : GoodProducts C ≃ range C :=
  Equiv.ofInjective (eval C) (injective C)

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