Icc_countable_iff — Mathlib

English

The closed interval [x,y] is countable iff y ≤ x.

Русский

Замкнутый интервал [x,y] счетен тогда и только тогда, когда y ≤ x.

LaTeX

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

Lean4

@[simp]
theorem Icc_countable_iff {x y : ℝ} : (Icc x y).Countable ↔ y ≤ x :=
  by
  refine
    ⟨fun h ↦ ?_, fun h ↦ by
      rcases le_iff_eq_or_lt.mp h with heq | hlt
      · simp [heq]
      · simp [hlt]⟩
  contrapose! h
  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]
  exact Cardinal.aleph0_lt_continuum

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