isCompact_Ioc_iff

Mathlib.Topology.Order.Compact

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

← MathLib Explorer

English

`Set.Ioc a b` is compact iff b ≤ a.

Русский

Множество Ioc a b компактно тогда и только тогда, когда b ≤ a.

LaTeX

$$IsCompact (Set.Ioc a b) ⇔ b ≤ a$$

Lean4

/-- `Set.Ioc a b` is only compact if it is empty. -/
@[simp]
theorem isCompact_Ioc_iff {a b : α} : IsCompact (Set.Ioc a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ioc_iff.mp h.isClosed, by simp_all⟩

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

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

Разделы

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

Аффилиация

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