infinite — Mathlib

English

In a densely ordered preorder, for any a < b, the interval Ioo(a, b) contains infinitely many points (the subtype is infinite).

Русский

В плотно упорядоченном порядке с a < b, интервал Ioo(a, b) содержит бесконечно много точек (подмножество бесконечно).

LaTeX

$$$\forall a,b\ (a

Lean4

theorem infinite : Infinite (Ioo a b) :=
  @NoMaxOrder.infinite _ _ (nonempty_Ioo_subtype h) _

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