English
There exists a CanLift from Set R to Subring R with the carrier predicate describing subring membership.
Русский
Существует CanLift из множества R в Subring R, задаваемый карманом по членству.
LaTeX
$$$ \\text{CanLift}( \\text{Set }R, \\text{Subring }R, \\uparrow, \\phi ) $$$
Lean4
instance (priority := 100) :
CanLift (Set R) (Subring 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 → -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
neg_mem' := h.2.2.2.2 }, rfl⟩
