English
Copying a NonUnitalStarSubsemiring with a new carrier equal to the old one preserves the underlying structure and star_mem property.
Русский
Копирование ненулевого звездного подполусемиринга с новым носителем, совпадающим с прежним, сохраняет структуру и свойство star_mem.
LaTeX
$$copy (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalStarSubsemiring R$$
Lean4
instance (priority := 100) :
CanLift (Set R) (NonUnitalStarSubsemiring 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 → star x ∈ s)
where
prf s
h :=
⟨{ carrier := s
zero_mem' := h.1
add_mem' := h.2.1
mul_mem' := h.2.2.1
star_mem' := h.2.2.2 }, rfl⟩
