of_universallyClosed_of_isDominant

English

If f is universally closed and dominant, then f is surjective.

Русский

Если морфизм f универсально замкнут и доминантен, тогда он сюръективен.

LaTeX

$$$\forall f:X\to Y,\; [\operatorname{UniversallyClosed}(f)] [\operatorname{IsDominant}(f)]\Rightarrow \operatorname{Surjective}(f).$$$

Lean4

instance (priority := low) of_universallyClosed_of_isDominant [UniversallyClosed f] [IsDominant f] : Surjective f := by
  rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range, f.isClosedMap.isClosed_range.closure_eq]

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