Ioc_countable_iff — Mathlib

English

The half-open interval (x,y] is countable iff y ≤ x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_countable_iff {x y : ℝ} : (Ioc 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_Ioc_real h, not_le]
  exact Cardinal.aleph0_lt_continuum

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