English
If a subset s ⊆ R contains 0 and is closed under addition, multiplication, and negation, then s is the carrier of a nonunital subsemiring of R (i.e., there exists a nonunital subsemiring with carrier s).
Русский
Если подмножество s ⊆ R содержит 0 и замыкется по сложению, умножению и взятию противоположного, то оно является носителем неединичного подполнечисления (неунитного подпомножества) R.
LaTeX
$$$0 \in s \wedge (\forall x,y \in s, x+y \in s) \wedge (\forall x,y \in s, x y \in s) \wedge (\forall x \in s, -x \in s) \Rightarrow \exists A : NonUnitalSubring(R), A.carrier = s$$$
Lean4
instance (priority := 100) :
CanLift (Set R) (NonUnitalSubring R) (↑)
(fun s ↦
0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → -x ∈ s)
where
prf s
h :=
⟨{ carrier := s
zero_mem' := h.1
add_mem' := h.2.1
mul_mem' := h.2.2.1
neg_mem' := h.2.2.2 }, rfl⟩
