injective_πs — Mathlib

English

The map πs' C h is injective for h: o1 ≤ o2, given appropriate surjectivity of the projection maps.

Русский

Отображение πs' C h инъективно при h: o1 ≤ o2, при подходящей сюръективности проекций.

LaTeX

$$$\\text{injective}(\\pi_s'\\,C\\,h).$$$

Lean4

theorem injective_πs (o : Ordinal) : Function.Injective (πs C o) :=
  LocallyConstant.comap_injective ⟨_, (continuous_projRestrict _ _)⟩ (Set.surjective_mapsTo_image_restrict _ _)

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