subsingleton — Mathlib

English

If 0 ∈ x, then the homogeneous localization HomogeneousLocalization 𝒜 x has at most one element (it is a subsingleton).

Русский

Если 0 ∈ x, то однородная локализация HomogeneousLocalization 𝒜 x содержит не более одного элемента (является одноэлементной).

LaTeX

$$$0 \in x \Rightarrow \operatorname{Subsingleton}(\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x))$$$

Lean4

theorem subsingleton (hx : 0 ∈ x) : Subsingleton (HomogeneousLocalization 𝒜 x) :=
  have := IsLocalization.subsingleton (S := at x) hx
  (HomogeneousLocalization.val_injective (𝒜 := 𝒜) (x := x)).subsingleton

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