sclosure_preimage_le — Mathlib

English

The preimage of a closure under a ring hom is contained in the closure of the preimage.

Русский

Образ предобраза замыкания через кольцевое отображение содержится в замыкании предобраза.

LaTeX

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

Lean4

theorem sclosure_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

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