English
For any subset s of A, the subalgebra generated by the preimage of s under the inclusion map from adjoin R s to A equals the top subalgebra.
Русский
Пусть s ⊆ A. Порождение подалгебры из предобраза s по включению из adjoin R s в A равно верхнему подалгебре.
LaTeX
$$$\\operatorname{adjoin}\\_R\\left( (\\uparrow)^{-1}(s) \\right) = \\top$$$
Lean4
@[simp]
theorem adjoin_adjoin_coe_preimage {s : Set A} : adjoin R (((↑) : adjoin R s → A) ⁻¹' s) = ⊤ :=
by
refine
eq_top_iff.2 fun ⟨x, hx⟩ ↦ adjoin_induction (fun a ha ↦ ?_) (fun r ↦ ?_) (fun _ _ _ _ ↦ ?_) (fun _ _ _ _ ↦ ?_) hx
· exact subset_adjoin ha
· exact Subalgebra.algebraMap_mem _ r
· exact Subalgebra.add_mem _
· exact Subalgebra.mul_mem _