English
There is a canonical lifting structure from Sets to StarSubsemirings: a subset s of a nonassociative semiring R whose carrier is closed under 0, addition, 1, multiplication, and star forms a StarSubsemiring.
Русский
Существует каноническое отображение из множеств в StarSubsemiring: подмножество s в полусложном полууравновешенном полугруппе R образует StarSubsemiring, если оно замкнуто по нуля, сложению, единице, умножению и звездному сопряжению.
LaTeX
$$$\text{CanLift}(\text{Set } R)(\text{StarSubsemiring } R)\uparrow (s \mapsto 0 \in s \land (\forall x,y\, x\in s\land y\in s\Rightarrow x+y\in s) \land 1\in s \land(\forall x,y\, x\in s\land y\in s\Rightarrow x\cdot y\in s) \land (\forall x\, x\in s\Rightarrow \star x \in s))$$$
Lean4
instance (priority := 100) :
CanLift (Set R) (StarSubsemiring 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) ∧ (∀ {x}, x ∈ s → star x ∈ 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.1
star_mem' := h.2.2.2.2 }, rfl⟩
