Ico_infinite — Mathlib

English

In a densely ordered α, for a < b, the half-open interval Ico(a, b) has infinitely many elements (the inclusion Ioo ⊆ Ico witnesses).

Русский

В плотно упорядоченном множестве α при a < b полуоткрытый интервал Ico(a, b) бесконечно большой по количеству элементов (Ioo ⊆ Ico помогает доказать).

LaTeX

$$$\forall a,b\ (a

Lean4

theorem Ico_infinite : (Ico a b).Infinite :=
  (Ioo_infinite h).mono Ioo_subset_Ico_self

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