nonempty_iff — Mathlib

English

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

Русский

Если функция f: α → X имеет плотный образ в X, то непустость α эквивалентна непустости X.

LaTeX

$$$ (\mathrm{DenseRange} \, f) \Rightarrow (\operatorname{Nonempty} \alpha \iff \operatorname{Nonempty} X)$$$

Lean4

nonrec theorem nonempty_iff (hf : DenseRange f) : Nonempty α ↔ Nonempty X :=
  range_nonempty_iff_nonempty.symm.trans hf.nonempty_iff

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