nonempty_Ico_subtype

Mathlib.Order.Interval.Set.Basic

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

English

If a < b, then the half-open interval Ico a b is nonempty (as a subtype).

Русский

Если a < b, то полузакрытый интервал Ico a b непуст как подпорядок.

LaTeX

$$$$ a < b \\Rightarrow \\mathrm{Nonempty}(\\mathrm{Ico} \\, a \\, b).\\Elem $$$$

Lean4

theorem nonempty_Ico_subtype (h : a < b) : Nonempty (Ico a b) :=
  Nonempty.to_subtype (nonempty_Ico.mpr h)

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

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

Разделы

Аффилиация

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