Ioi_ssubset_Ioi_iff

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

Ioi b is a strict subset of Ioi a if and only if a < b.

Русский

Ioi b есть строгим подмножеством Ioi a тогда и только тогда a < b.

LaTeX

$$$ Ioi(b) \subset Ioi(a) \iff a < b $$$

Lean4

@[simp]
theorem Ioi_ssubset_Ioi_iff : Ioi b ⊂ Ioi a ↔ a < b :=
  by
  refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
  obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h
  exact ac.trans_le (le_of_not_gt cb)

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

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

Разделы

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

Аффилиация

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