denseRange_discrete

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#denseRange_discrete

English

For a function f: ι → α into a discrete space, DenseRange f holds iff f is surjective.

Русский

Для функции f: ι → α в дискретном пространстве DenseRange f эквивалентно сюрjektивности.

LaTeX

$${DenseRange f} ⇔ {Surjective f}$$

Lean4

@[simp]
theorem denseRange_discrete {ι : Type*} {f : ι → α} : DenseRange f ↔ Surjective f := by
  rw [DenseRange, dense_discrete, range_eq_univ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru