J_le_monomorphisms — Mathlib

English

The class J is contained in the class of monomorphisms; any morphism in J is mono.

Русский

Класс J содержится в мономорфизмах; любой морфизм в J является монообразом.

LaTeX

$$$ J \\subseteq \\mathrm{Monomorphisms}$$$

Lean4

theorem J_le_monomorphisms : J.{u} ≤ monomorphisms _ :=
  by
  rintro _ _ _ h
  simp only [J, iSup_iff] at h
  obtain ⟨n, ⟨i⟩⟩ := h
  exact monomorphisms.infer_property _

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