nonempty

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#DenseRange.nonempty

English

If X is nonempty and f: α → X has dense range in X, then α is nonempty.

Русский

Если X непусто и f: α → X имеет плотный образ, то α непусто.

LaTeX

$$(\mathrm{DenseRange} \ f) \rightarrow \operatorname{Nonempty} X \rightarrow \operatorname{Nonempty} \alpha$$

Lean4

theorem nonempty [h : Nonempty X] (hf : DenseRange f) : Nonempty α :=
  hf.nonempty_iff.mpr h

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

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

Разделы

Аффилиация

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