surjective_transitionMapLE — Mathlib

English

For any h with n ≤ m, the map S.transitionMapLE h is surjective.

Русский

Для любого h с n ≤ m переходная карта LE h сюръективна.

LaTeX

$$$\forall {n,m:\mathbb{N}}(h:\,n\le m), \; S.transitionMapLE(h) \text{ is surjective}$$$

Lean4

theorem surjective_transitionMapLE {n m : ℕ} (h : n ≤ m) : Function.Surjective (S.transitionMapLE h) :=
  by
  apply Function.Surjective.of_comp (g := S.proj m)
  simpa only [proj_comp_transitionMapLE'] using S.proj_surjective n

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