Ico_subset

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.Ico_subset

English

If a ⩿ b, then Ico(a,b) is contained in {a}, i.e., there are no interior points strictly between a and b.

Русский

Если a ⩿ b, то Ico(a,b) вложено в {a}, то есть между a и b нет промежуточных точек.

LaTeX

$$$$Ico(a,b)\subseteq\{a\}.$$$$

Lean4

theorem Ico_subset (h : a ⩿ b) : Ico a b ⊆ { a } := by
  rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]

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

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

Разделы

Аффилиация

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