left_mem_openSegment_iff — Mathlib

English

In a densely ordered ring with appropriate conditions, the left endpoint membership characterizes equality with the left endpoint: x ∈ openSegment 𝕜 x y iff x = y.

Русский

При плотном порядке и подходящих условиях членство слева в openSegment 𝕜 x y эквивалентно x = y.

LaTeX

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

Lean4

@[simp]
theorem left_mem_openSegment_iff [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : x ∈ openSegment 𝕜 x y ↔ x = y :=
  by
  constructor
  · rintro ⟨a, b, _, hb, hab, hx⟩
    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)
    rw [hx, ← add_smul, hab, one_smul]
  · rintro rfl
    rw [openSegment_same]
    exact mem_singleton _

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