exists_gt

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.exists_gt

← MathLib Explorer

English

There exists a ∈ α with f < const a.

Русский

Существует a ∈ α такое, что f < const a.

LaTeX

$$$\exists a \in \alpha,\; f < \mathrm{const}(a).$$$

Lean4

theorem exists_gt (f : CauSeq α abs) : ∃ a : α, f < const a :=
  let ⟨K, H⟩ := f.bounded
  ⟨K + 1, 1, zero_lt_one, 0, fun i _ =>
    by
    rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]
    exact le_of_lt (abs_lt.1 (H _)).2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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