infinite_of_forall_exists_lt

Mathlib.Order.Preorder.Finite

URI: https://scilib.ai/kg/mathlib#Set.infinite_of_forall_exists_lt

English

If for every a there exists b ∈ s with b < a in a preorder, then s is infinite.

Русский

Если для каждого a существует b ∈ s такой, что b < a, то s бесконечно.

LaTeX

$$$\forall a\,\exists b\ (b \in s \wedge b < a) \Rightarrow s \text{ is infinite}.$$$

Lean4

theorem infinite_of_forall_exists_lt (h : ∀ a, ∃ b ∈ s, b < a) : s.Infinite :=
  infinite_of_forall_exists_gt (α := αᵒᵈ) h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru