closure_preimage_le — Mathlib

English

For a monoid homomorphism f and a set s in the codomain, the closure of the preimage f^{-1}(s) maps into the preimage under f of the closure of s.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem closure_preimage_le (f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  (closure_le _).2 fun x hx => by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx

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