isClosedMap_iff_kernImage_interior

English

IsClosedMap f is equivalent to KernImage interior criterion with a simp closure relation.

Русский

IsClosedMap f эквивалентно условию KernImage interior с упрощённой связью замыкания.

LaTeX

$$$IsClosedMap f \\iff \\forall {s}, kernImage f (interior s) ⊆ interior (kernImage f s)$$$

Lean4

theorem isClosedMap_iff_kernImage_interior :
    IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s) :=
  by
  rw [isClosedMap_iff_closure_image, compl_surjective.forall]
  simp [kernImage_eq_compl]

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