range_equiv_smaller_toFun_bijective

English

The map from the range to the smaller object is bijective.

Русский

Отображение отобразиующее диапазон к меньшему объекту биективно.

LaTeX

$$$$\\mathrm{Function.Bijective}\\; (\\mathrm{range\\_equiv\\_smaller\\_toFun}\\; C\\; o)$$$$

Lean4

theorem range_equiv_smaller_toFun_bijective (o : Ordinal) : Function.Bijective (range_equiv_smaller_toFun C o) :=
  by
  dsimp +unfoldPartialApp [range_equiv_smaller_toFun]
  refine ⟨fun a b hab ↦ ?_, fun ⟨a, b, hb⟩ ↦ ?_⟩
  · ext1
    simp only [Subtype.mk.injEq] at hab
    exact injective_πs C o hab
  · use ⟨b, hb.1⟩
    simpa only [Subtype.mk.injEq] using hb.2

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