surjective_transitionMap — Mathlib

English

For every n, the bonding map S.transitionMap n is surjective on points.

Русский

Для каждого n переходная карта S.transitionMap n на уровне точек сюръективна.

LaTeX

$$$\forall n \in \mathbb{N}, \; S.transitionMap(n) \\text{ is surjective}$$$

Lean4

theorem surjective_transitionMap (n : ℕ) : Function.Surjective (S.transitionMap n) :=
  by
  apply Function.Surjective.of_comp (g := S.proj (n + 1))
  simpa only [proj_comp_transitionMap'] using S.proj_surjective n

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