exists_countable_dense_no_zero_top

English

There exists a countable subset s of ℝ≥0∞ which is dense and does not contain 0 or ∞.

Русский

Существует счетное плотное подмножество s ⊆ ℝ≥0∞, не содержащее 0 и бесконечность.

LaTeX

$$$\\exists s \\subseteq \\mathbb{R}_{\\ge 0}^{\\infty},\\ s\\ \\text{Countable} \\land s\\ \\text{Dense} \\land 0 \\notin s \\land \\infty \\notin s.$$$

Lean4

theorem exists_countable_dense_no_zero_top : ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s :=
  by
  obtain ⟨s, s_count, s_dense, hs⟩ :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
    exists_countable_dense_no_bot_top ℝ≥0∞
  exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩

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