closure_preimage_le — Mathlib

English

For a function f: F and s ⊆ S, closure ((f: R → S)⁻¹' s) ≤ (closure s).comap f.

Русский

Для произвольной функции f и множества s, замыкание предобраза f по s вложено в обратный образ замыкания s по f.

LaTeX

$$$\overline{(f: R \to S)^{-1}(s)} \le (\overline{s}).comap f$$$

Lean4

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

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