range_equiv — Mathlib

English

There is a canonical equivalence between the range of C and the union of smaller_C indexed by ordinals below o.

Русский

Существет каноническое эквивалентность между образами C и объединением smaller_C, индексируемым ординалами ниже o.

LaTeX

$$$\\operatorname{range}(C) \\simeq \\bigcup_{e:\\{ o'\\;\\|\\;o'

Lean4

/-- The image of the `GoodProducts` in `C` is equivalent to the union of `smaller C o'` over all
ordinals `o' < o`.
-/
def range_equiv : range C ≃ ⋃ (e : { o' // o' < o }), (smaller C e.val) :=
  Equiv.setCongr (union C ho hsC)

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