len_le_of_mono — Mathlib

English

Let f: x → y be a mono morphism in the Simplex category. Then x.len ≤ y.len.

Русский

Пусть f: x → y — моно морфизм в категорий Simplex. Тогда x.len ≤ y.len.

LaTeX

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

Lean4

/-- A monomorphism in `SimplexCategory` must increase lengths -/
theorem len_le_of_mono {x y : SimplexCategory} (f : x ⟶ y) [Mono f] : x.len ≤ y.len := by
  simpa using Fintype.card_le_of_injective f.toOrderHom.toFun (by dsimp; rwa [← mono_iff_injective])

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