right_mem_of_mem_openSegment — Mathlib

English

If A is extreme with respect to B and x ∈ A, y ∈ A, z ∈ B with z in openSegment(x,y), then y ∈ B.

Русский

Если A экстремально связана с B и z лежит в открытом сегменте между x и y, то y ∈ B.

LaTeX

$$$$ \text{IsExtreme } 𝕜\ A\ B \to (x,y,z) \in A\times A\times B,\ z \in openSegment 𝕜 x y \Rightarrow y \in B. $$$$

Lean4

theorem right_mem_of_mem_openSegment (h : IsExtreme 𝕜 A B) {y z : E} (hx : x ∈ A) (hy : y ∈ A) (hz : z ∈ B)
    (hzxy : z ∈ openSegment 𝕜 x y) : y ∈ B :=
  h.left_mem_of_mem_openSegment hy hx hz <| by rwa [openSegment_symm]

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