of_nonempty — Mathlib

English

If f is a closed map and h holds a certain property for all nonempty closed s, then f is a closed map.

Русский

Если f — замкнутое отображение и существует условие на все непустые замкнутые множества s, то f — замкнутое отображение.

LaTeX

$$$IsClosedMap f \\to \\forall s, IsClosed s \\to s.Nonempty \\to IsClosed (f''s)$$$

Lean4

theorem of_nonempty (h : ∀ s, IsClosed s → s.Nonempty → IsClosed (f '' s)) : IsClosedMap f :=
  by
  intro s hs; rcases eq_empty_or_nonempty s with h2s | h2s
  · simp_rw [h2s, image_empty, isClosed_empty]
  · exact h s hs h2s

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