isomorphisms_le — Mathlib

English

There is a comparison between isomorphisms of D and the relatively representable morphisms given by F.

Русский

Существует некое соотношение изоморфизмов D и относительно представимых морфизмов, задаваемое F.

LaTeX

$$$$\\text{isomorphisms}(D) \\le F.relativelyRepresentable$$$$

Lean4

theorem isomorphisms_le : MorphismProperty.isomorphisms D ≤ F.relativelyRepresentable := fun _ _ f hf ↦
  letI : IsIso f := hf;
  of_isIso F f

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