segment_eq_Icc'

Mathlib.Analysis.Convex.Segment

URI: https://scilib.ai/kg/mathlib#segment_eq_Icc'

← MathLib Explorer

English

segment 𝕜 x y equals Icc(min{x,y}, max{x,y}).

Русский

segment 𝕜 x y равен Icc(min{x,y}, max{x,y}).

LaTeX

$$$ segment_{\mathbb{k}}(x,y) = Icc(\min\{x,y\}, \max\{x,y\}) $$$

Lean4

theorem segment_eq_Icc' (x y : 𝕜) : [x -[𝕜] y] = Icc (min x y) (max x y) :=
  by
  rcases le_total x y with h | h
  · rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
  · rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]

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

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

Разделы

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

Аффилиация

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