English
If x has support contained in s, then applying restriction on s and then the inclusion map recovers x: map(↑) (restriction s x) = x.
Русский
Если x имеет опору в пределах s, то применение ограничения на s и затем включение обратно возвращает x:
LaTeX
$$$\\text{If } hxs : \\mathrm{IsSupported}(x, s),\\quad \\mathrm{map}(\\uparrow)(\\mathrm{restriction}(s)(x)) = x$$$
Lean4
theorem map_subtype_val_restriction {x} (s : Set α) [DecidablePred (· ∈ s)] (hxs : IsSupported x s) :
map (↑) (restriction s x) = x :=
by
refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
· rw [RingHom.map_one]
rfl
· rw [map_neg, map_one]
rfl
· rintro _ ⟨p, hps, rfl⟩ n ih
rw [RingHom.map_mul, restriction_of, dif_pos hps, RingHom.map_mul, map_of, ih]
· intro x y ihx ihy
rw [RingHom.map_add, RingHom.map_add, ihx, ihy]
