le_of_mono

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.le_of_mono

← MathLib Explorer

English

If f: ⟨n⟩ → ⟨m⟩ is mono, then n ≤ m.

Русский

Если f: ⟨n⟩ → ⟨m⟩ моно, тогда n ≤ m.

LaTeX

$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\forall f: \\\\langle n \\\\rangle \\\\to \\\\langle m \\\\rangle,[\\\\text{Mono } f] \\\Rightarrow n \\\\le m$$$

Lean4

theorem le_of_mono {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌) [Mono f] : n ≤ m :=
  len_le_of_mono f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru