isClosedMap — Mathlib

English

IsClosedMap f is equivalent to KernImage interior condition: f is closed iff kernImage f (interior s) ⊆ interior (kernImage f s) for all s.

Русский

IsClosedMap f эквивалентно условию kernImage внутри: f замкнуто тогда и только тогда, когда kernImage f (interior s) ⊆ interior (kernImage f s) для всех s.

LaTeX

$$$IsClosedMap f \\iff ∀ {s}, kernImage f (\\operatorname{int} s) \\subseteq \\operatorname{int}(kernImage f s)$$$

Lean4

theorem isClosedMap (hf : IsInducing f) (h : IsClosed (range f)) : IsClosedMap f :=
  by
  intro s hs
  rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
  rw [image_preimage_eq_inter_range]
  exact ht.inter h

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