injective_πs' — Mathlib

English

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

Русский

πs' C h инъективно при h: o1 ≤ o2, при сюръективности проекций.

LaTeX

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

Lean4

theorem injective_πs' {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) : Function.Injective (πs' C h) :=
  LocallyConstant.comap_injective ⟨_, (continuous_projRestricts _ _)⟩
    (surjective_projRestricts _ fun _ hi ↦ lt_of_lt_of_le hi h)

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