proj_surjective — Mathlib

English

For every natural number n, the projection S.proj n is surjective (on the level of maps after passage to the appropriate forgetful functor).

Русский

Для каждого натурального числа n отображение проекции S.proj n сюръективно (после применения соответствующего забывающего функторa).

LaTeX

$$$\\forall n:\\mathbb{N},\\; \\mathrm{Function.Surjective}(S.proj(n)).$$$

Lean4

theorem proj_surjective (n : ℕ) : Function.Surjective (S.proj n) :=
  by
  change Function.Surjective (lightToProfinite.map (S.proj n))
  rw [lightToProfinite_map_proj_eq]
  exact DiscreteQuotient.proj_surjective _

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