closure_preimage_le — Mathlib

English

For a ring homomorphism f: R → S and a subset s ⊆ S, the closure of the preimage f^{-1}(s) is contained in the comap of the closure of s along f.

Русский

Для гомоморфизма колец f: R → S и подмножества s ⊆ S, замыкание предобраза f^{-1}(s) содержится в обратном образе замыкания s по f.

LaTeX

$$$ \operatorname{closure}(f^{-1}(s)) \le (\operatorname{closure}(s)).\mathrm{comap}\ f $$$

Lean4

theorem closure_preimage_le (f : R →+* S) (s : Set S) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Похожие утверждения