exists_rat_mem_uIoo

Mathlib.Algebra.Order.Archimedean.Basic

URI: https://scilib.ai/kg/mathlib#exists_rat_mem_uIoo

English

If x ≠ y, there exists a rational q such that q.cast lies strictly between x and y.

Русский

Если x ≠ y, то существует рациональное q, такое что q.cast лежит строго между x и y.

LaTeX

$$$\exists q\in\mathbb{Q},\ x < q.cast \land q.cast < y$$$

Lean4

theorem exists_rat_mem_uIoo {x y : K} (h : x ≠ y) : ∃ q : ℚ, ↑q ∈ Set.uIoo x y :=
  exists_rat_btwn (min_lt_max.mpr h)

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

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

Разделы

Аффилиация

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