English
An instance ensuring that a subset closed under 0, addition, and multiplication lifts to a nonunital subsemiring with the same carrier.
Русский
Инстанс обеспечивает перенос множества, замкнутого относительно 0, сложения и умножения, в неединичное подпполе с тем же носителем.
LaTeX
$$CanLift (Set R) (NonUnitalSubsemiring R) (↑) (fun s => 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) $$
Lean4
instance (priority := 100) :
CanLift (Set R) (NonUnitalSubsemiring R) (↑)
(fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ 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
mul_mem' := h.2.2 }, rfl⟩
