nonempty_iff — Mathlib

English

A dense subset s is nonempty if and only if the ambient space X is nonempty.

Русский

Плотное подмножество s непусто тогда и только тогда, когда пространство X непусто.

LaTeX

$$$\operatorname{Dense}(s) \rightarrow (s \neq \emptyset \iff X \neq \emptyset)$$$

Lean4

theorem nonempty_iff (hs : Dense s) : s.Nonempty ↔ Nonempty X :=
  ⟨fun ⟨x, _⟩ => ⟨x⟩, fun ⟨x⟩ =>
    let ⟨y, hy⟩ := hs.inter_open_nonempty _ isOpen_univ ⟨x, trivial⟩
    ⟨y, hy.2⟩⟩

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