mclosure_preimage_le — Mathlib

English

For f : M →* N and s ⊆ N, closure(f^{-1}(s)) ≤ closure(s) comapped along f.

Русский

Для f : M →* N и подмножества s ⊆ N верно: closure(f^{-1}(s)) ≤ closure(s) ∘ f.

LaTeX

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

Lean4

@[to_additive]
theorem mclosure_preimage_le (f : F) (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

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