containsIdentities — Mathlib

English

If a localization-away property holds for P, then P contains all identities (i.e., identity morphisms satisfy P).

Русский

Если локализационная установка для P выполняется, то P содержит все тождественные отображения.

LaTeX

$$$\\text{HoldsForLocalizationAway}(P) \\Rightarrow \\text{ContainsIdentities}(P)$$$

Lean4

theorem containsIdentities (hPl : HoldsForLocalizationAway P) : ContainsIdentities P :=
  by
  introv R
  exact hPl.of_bijective _ _ Function.bijective_id

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