English
For any ring R, the operator RingCone R admits a SetLike structure, identifying RingCones with subsets of R via their carriers, and the coejection is injective.
Русский
Для кольца R множество RingCone R допускает структуру SetLike: RingCone связывает конусы с подмножествами R через переносчик, и сопоставление инъективно.
LaTeX
$$$ \\forall R [\\text{Ring } R],\\; \\text{RingCone}(R) \\text{ has a SetLike structure with } C \\mapsto \\operatorname{carrier}(C) \\text{ and } \\operatorname{carrier}(C) = \\operatorname{carrier}(D) \\Rightarrow C = D.$$$
Lean4
instance instSetLike (R : Type*) [Ring R] : SetLike (RingCone R) R
where
coe C := C.carrier
coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
