affineSegment_comm — Mathlib

English

The affine segment is symmetric in its endpoints: affineSegment(R, x, y) = affineSegment(R, y, x).

Русский

Афинный отрезок симметричен относительно концов: affineSegment(R, x, y) = affineSegment(R, y, x).

LaTeX

$$$\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,y,x).$$$

Lean4

theorem affineSegment_comm (x y : P) : affineSegment R x y = affineSegment R y x :=
  by
  refine Set.ext fun z => ?_
  constructor <;>
    · rintro ⟨t, ht, hxy⟩
      refine ⟨1 - t, ?_, ?_⟩
      · rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
      · rwa [lineMap_apply_one_sub]

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