mclosure_preimage_le — Mathlib

English

Let f: M → N be a semigroup hom and S a subset of N. Then the subsemigroup generated by the preimage f^{-1}(S) inside M is contained in the preimage under f of the subsemigroup generated by S in N.

Русский

Пусть f: M → N — гомоморфизм полугрупп и S ⊆ N. Тогда подполугруппа, порождается множеством f^{-1}(S) в M, содержится в обратном образе f^{-1}(замыкания(S)); эквивалентно closure(f^{-1}(S)) ⊆ f^{-1}(closure(S)).

LaTeX

$$$\\operatorname{closure}(f^{-1}(s)) \\subseteq f^{-1}(\\operatorname{closure}(s))$$$

Lean4

@[to_additive]
theorem mclosure_preimage_le (f : M →ₙ* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

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