Icc_inter_Icc_eq_singleton

Mathlib.Order.Interval.Set.Basic

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

← MathLib Explorer

English

If a ≤ b ≤ c, then Icc(a,b) ∩ Icc(b,c) = {b}.

Русский

Если a ≤ b ≤ c, то Icc(a,b) ∩ Icc(b,c) = {b}.

LaTeX

$$$$ a \\le b \\le c \\Rightarrow Icc(a,b) \\cap Icc(b,c) = \\{b\\} $$$$

Lean4

@[simp]
theorem Icc_inter_Icc_eq_singleton (hab : a ≤ b) (hbc : b ≤ c) : Icc a b ∩ Icc b c = { b } :=
  by
  rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]
  simp [hab, hbc]

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

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

Разделы

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

Аффилиация

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