English
A subset s of a semiring R that contains 0 and 1, and is closed under addition and multiplication, is the carrier of a subsemiring of R.
Русский
Подмножество s тождественно образует подпол semiring внутри R, если 0 и 1 принадлежат s и s замкнуто относительно сложения и умножения.
LaTeX
$$$\bigl(0 \in s \ \land\ 1 \in s \ \land\ \forall x,y\in s:\ x+y \in s \land x\cdot y \in s\bigr) \Rightarrow \exists S:\text{Subsemiring}(R), \operatorname{carrier}(S)=s$$$
Lean4
instance (priority := 100) :
CanLift (Set R) (Subsemiring R) (↑)
(fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s)
where
prf s
h :=
⟨{ carrier := s
zero_mem' := h.1
add_mem' := h.2.1
one_mem' := h.2.2.1
mul_mem' := h.2.2.2 }, rfl⟩
