le_of_epi — Mathlib

English

For natural numbers n,m and epi f: ⟦n⟧ → ⟦m⟧, we have m ≤ n.

Русский

Для натуральных чисел n,m и эпиморфизма f: ⟦n⟧ → ⟦m⟧ имеет место m ≤ n.

LaTeX

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

Lean4

theorem le_of_epi {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] : m ≤ n :=
  len_le_of_epi f

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