of_injective — Mathlib

English

If N has finite length and f: M → N is injective, then M has finite length.

Русский

Если N имеет конечную длину и отображение f: M → N инъективно, то M тоже имеет конечную длину.

LaTeX

$$$\\displaystyle \\text{IsFiniteLength } R N \\land \\text{Function.Injective } f \\Rightarrow \\text{IsFiniteLength } R M$$$

Lean4

theorem of_injective (H : IsFiniteLength R N) (hf : Function.Injective f) : IsFiniteLength R M :=
  by
  rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢
  cases H
  exact ⟨isNoetherian_of_injective f hf, isArtinian_of_injective f hf⟩

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