exists_gt

Mathlib.Order.Interval.Finset.Basic

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

English

If s is an infinite subset of α, then for every a ∈ α there exists b ∈ s with a < b.

Русский

Если s — бесконечно множество подмножество α, то для любого a ∈ α существует b ∈ s such that a < b.

LaTeX

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

Lean4

theorem _root_.Set.Infinite.exists_gt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, a < b :=
  not_bddAbove_iff.1 hs.not_bddAbove

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

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

Разделы

Аффилиация

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