surjective_of_isDominant_of_isClosed_range

English

If f: X → Y is dominant and the underlying map has closed range, then f is surjective.

Русский

Если f: X → Y доминирует, а образ базового отображения замкнут, то f сюръективен.

LaTeX

$$$\\mathrm{IsDominant}(f) \\land \\mathrm{IsClosed}(\\mathrm{range}(f_{\\mathrm{base}})) \\Rightarrow \\mathrm{Surjective}(f)$$$

Lean4

theorem surjective_of_isDominant_of_isClosed_range (f : X ⟶ Y) [IsDominant f] (hf : IsClosed (Set.range f.base)) :
    Surjective f :=
  ⟨by rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]⟩

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