sclosure_preimage_le — Mathlib

English

Another formulation of the previous fact about closure of preimages under a map.

Русский

Ещё одно формулирование предыдущего факта о замыкании предобраза под отображением.

LaTeX

$$closure ((f : R → S) ⁻¹' s) ≤ (closure s).comap f$$

Lean4

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

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