Ioo_countable_iff — Mathlib

English

The open interval (x,y) is countable if and only if y ≤ x.

Русский

Открытый интервал (x,y) счетен тогда и только тогда, когда y ≤ x.

LaTeX

$$$(Ioo\ x\ y).Countable \Leftrightarrow y \le x$$$

Lean4

@[simp]
theorem Ioo_countable_iff {x y : ℝ} : (Ioo x y).Countable ↔ y ≤ x :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  contrapose! h
  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]
  exact Cardinal.aleph0_lt_continuum

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