right_mem_openSegment_iff

Mathlib.Analysis.Convex.Segment

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

← MathLib Explorer

English

Symmetric statement: y ∈ openSegment 𝕜 x y iff x = y.

Русский

Симметричное утверждение: y ∈ openSegment 𝕜 x y ⇔ x = y.

LaTeX

$$$$ y \in openSegment_{\mathbb{K}}(x,y) \iff x = y. $$$$

Lean4

@[simp]
theorem right_mem_openSegment_iff [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : y ∈ openSegment 𝕜 x y ↔ x = y := by
  rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

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

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

Разделы

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

Аффилиация

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