dominant_eq_topologically — Mathlib

English

IsDominant is equivalent to topologically DenseRange; the dominance of a morphism equals the density of its image in the topological sense.

Русский

Свойство упорядочения доминантности эквивалентно плотности образа в топологическом смысле; изоморфизм доминирует тогда и только тогда, когда образ плотный.

LaTeX

$$$IsDominant = topologically DenseRange$$$

Lean4

theorem dominant_eq_topologically : @IsDominant = topologically DenseRange := by ext; exact isDominant_iff _

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