len_le_of_epi — Mathlib

English

An epimorphism f: x → y in the Simplex category forces y.len ≤ x.len.

Русский

Эпиморфизм f: x → y в SimplexCategory приводит к y.len ≤ x.len.

LaTeX

$$$\\\\forall {x,y: \\\\text{SimplexCategory}}\\\\forall f: x \\\\to y,[\\\\text{Epi } f] \\\Rightarrow y.len \\\\le x.len$$$

Lean4

/-- An epimorphism in `SimplexCategory` must decrease lengths -/
theorem len_le_of_epi {x y : SimplexCategory} (f : x ⟶ y) [Epi f] : y.len ≤ x.len := by
  simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun (by dsimp; rwa [← epi_iff_surjective])

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