exists_lt

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Set.Infinite.exists_lt

English

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

Русский

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

LaTeX

$$|s| = \infty \Rightarrow \forall a, \exists b \in s, b < a$$

Lean4

theorem _root_.Set.Infinite.exists_lt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, b < a :=
  not_bddBelow_iff.1 hs.not_bddBelow

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

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

Разделы

Аффилиация

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