injective_iff — Mathlib

English

For a localization map f : S.LocalizationMap N, f is injective if and only if every element x ∈ S is regular (i.e., is left cancellable) in the ambient monoid.

Русский

Для отображения локализации f : S.LocalizationMap N: f инъективно тогда и только тогда, когда каждый элемент x ∈ S является регулярным (левая отменяемость) в исходном моноиде.

LaTeX

$$$\\text{Injective}(f) \\iff \\forall x\\,(x \\in S \\rightarrow \\text{IsRegular}(x))$$$

Lean4

@[to_additive]
theorem injective_iff (f : LocalizationMap S N) : Injective f ↔ ∀ ⦃x⦄, x ∈ S → IsRegular x :=
  by
  simp_rw [Commute.isRegular_iff (Commute.all _), IsLeftRegular, Injective, LocalizationMap.eq_iff_exists, exists_imp,
    Subtype.forall]
  exact forall₂_swap

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