Documentation

Mathlib.Analysis.Convex.Side

Sides of affine subspaces #

This file defines notions of two points being on the same or opposite sides of an affine subspace.

Main definitions #

def AffineSubspace.WSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) (y : P) :

The points x and y are weakly on the same side of s.

Equations
  • s.WSameSide x y = p₁s, p₂s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Instances For
    def AffineSubspace.SSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) (y : P) :

    The points x and y are strictly on the same side of s.

    Equations
    • s.SSameSide x y = (s.WSameSide x y xs ys)
    Instances For
      def AffineSubspace.WOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) (y : P) :

      The points x and y are weakly on opposite sides of s.

      Equations
      • s.WOppSide x y = p₁s, p₂s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
      Instances For
        def AffineSubspace.SOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) (y : P) :

        The points x and y are strictly on opposite sides of s.

        Equations
        • s.SOppSide x y = (s.WOppSide x y xs ys)
        Instances For
          theorem AffineSubspace.WSameSide.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WSameSide x y) (f : P →ᵃ[R] P') :
          (AffineSubspace.map f s).WSameSide (f x) (f y)
          theorem Function.Injective.wSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
          (AffineSubspace.map f s).WSameSide (f x) (f y) s.WSameSide x y
          theorem Function.Injective.sSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
          (AffineSubspace.map f s).SSameSide (f x) (f y) s.SSameSide x y
          @[simp]
          theorem AffineEquiv.wSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (f : P ≃ᵃ[R] P') :
          (AffineSubspace.map (f) s).WSameSide (f x) (f y) s.WSameSide x y
          @[simp]
          theorem AffineEquiv.sSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (f : P ≃ᵃ[R] P') :
          (AffineSubspace.map (f) s).SSameSide (f x) (f y) s.SSameSide x y
          theorem AffineSubspace.WOppSide.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WOppSide x y) (f : P →ᵃ[R] P') :
          (AffineSubspace.map f s).WOppSide (f x) (f y)
          theorem Function.Injective.wOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
          (AffineSubspace.map f s).WOppSide (f x) (f y) s.WOppSide x y
          theorem Function.Injective.sOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
          (AffineSubspace.map f s).SOppSide (f x) (f y) s.SOppSide x y
          @[simp]
          theorem AffineEquiv.wOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (f : P ≃ᵃ[R] P') :
          (AffineSubspace.map (f) s).WOppSide (f x) (f y) s.WOppSide x y
          @[simp]
          theorem AffineEquiv.sOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x : P} {y : P} (f : P ≃ᵃ[R] P') :
          (AffineSubspace.map (f) s).SOppSide (f x) (f y) s.SOppSide x y
          theorem AffineSubspace.WSameSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WSameSide x y) :
          (s).Nonempty
          theorem AffineSubspace.SSameSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          (s).Nonempty
          theorem AffineSubspace.WOppSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WOppSide x y) :
          (s).Nonempty
          theorem AffineSubspace.SOppSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          (s).Nonempty
          theorem AffineSubspace.SSameSide.wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          s.WSameSide x y
          theorem AffineSubspace.SSameSide.left_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          xs
          theorem AffineSubspace.SSameSide.right_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          ys
          theorem AffineSubspace.SOppSide.wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          s.WOppSide x y
          theorem AffineSubspace.SOppSide.left_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          xs
          theorem AffineSubspace.SOppSide.right_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          ys
          theorem AffineSubspace.wSameSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WSameSide x y s.WSameSide y x
          theorem AffineSubspace.WSameSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WSameSide x ys.WSameSide y x

          Alias of the forward direction of AffineSubspace.wSameSide_comm.

          theorem AffineSubspace.sSameSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.SSameSide x y s.SSameSide y x
          theorem AffineSubspace.SSameSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.SSameSide x ys.SSameSide y x

          Alias of the forward direction of AffineSubspace.sSameSide_comm.

          theorem AffineSubspace.wOppSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WOppSide x y s.WOppSide y x
          theorem AffineSubspace.WOppSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WOppSide x ys.WOppSide y x

          Alias of the forward direction of AffineSubspace.wOppSide_comm.

          theorem AffineSubspace.sOppSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.SOppSide x y s.SOppSide y x
          theorem AffineSubspace.SOppSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.SOppSide x ys.SOppSide y x

          Alias of the forward direction of AffineSubspace.sOppSide_comm.

          theorem AffineSubspace.not_wSameSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :
          ¬.WSameSide x y
          theorem AffineSubspace.not_sSameSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :
          ¬.SSameSide x y
          theorem AffineSubspace.not_wOppSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :
          ¬.WOppSide x y
          theorem AffineSubspace.not_sOppSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :
          ¬.SOppSide x y
          @[simp]
          theorem AffineSubspace.wSameSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} :
          s.WSameSide x x (s).Nonempty
          theorem AffineSubspace.sSameSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} :
          s.SSameSide x x (s).Nonempty xs
          theorem AffineSubspace.wSameSide_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x s) :
          s.WSameSide x y
          theorem AffineSubspace.wSameSide_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} (x : P) {y : P} (hy : y s) :
          s.WSameSide x y
          theorem AffineSubspace.wOppSide_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x s) :
          s.WOppSide x y
          theorem AffineSubspace.wOppSide_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} (x : P) {y : P} (hy : y s) :
          s.WOppSide x y
          theorem AffineSubspace.wSameSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.WSameSide (v +ᵥ x) y s.WSameSide x y
          theorem AffineSubspace.wSameSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.WSameSide x (v +ᵥ y) s.WSameSide x y
          theorem AffineSubspace.sSameSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.SSameSide (v +ᵥ x) y s.SSameSide x y
          theorem AffineSubspace.sSameSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.SSameSide x (v +ᵥ y) s.SSameSide x y
          theorem AffineSubspace.wOppSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.WOppSide (v +ᵥ x) y s.WOppSide x y
          theorem AffineSubspace.wOppSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.WOppSide x (v +ᵥ y) s.WOppSide x y
          theorem AffineSubspace.sOppSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.SOppSide (v +ᵥ x) y s.SOppSide x y
          theorem AffineSubspace.sOppSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {v : V} (hv : v s.direction) :
          s.SOppSide x (v +ᵥ y) s.SOppSide x y
          theorem AffineSubspace.wSameSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ : P} {p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 t) :
          s.WSameSide (t (x -ᵥ p₁) +ᵥ p₂) x
          theorem AffineSubspace.wSameSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ : P} {p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 t) :
          s.WSameSide x (t (x -ᵥ p₁) +ᵥ p₂)
          theorem AffineSubspace.wSameSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : 0 t) :
          s.WSameSide ((AffineMap.lineMap x y) t) y
          theorem AffineSubspace.wSameSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : 0 t) :
          s.WSameSide y ((AffineMap.lineMap x y) t)
          theorem AffineSubspace.wOppSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ : P} {p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t 0) :
          s.WOppSide (t (x -ᵥ p₁) +ᵥ p₂) x
          theorem AffineSubspace.wOppSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ : P} {p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t 0) :
          s.WOppSide x (t (x -ᵥ p₁) +ᵥ p₂)
          theorem AffineSubspace.wOppSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : t 0) :
          s.WOppSide ((AffineMap.lineMap x y) t) y
          theorem AffineSubspace.wOppSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : t 0) :
          s.WOppSide y ((AffineMap.lineMap x y) t)
          theorem Wbtw.wSameSide₂₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hx : x s) :
          s.WSameSide y z
          theorem Wbtw.wSameSide₃₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hx : x s) :
          s.WSameSide z y
          theorem Wbtw.wSameSide₁₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hz : z s) :
          s.WSameSide x y
          theorem Wbtw.wSameSide₂₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hz : z s) :
          s.WSameSide y x
          theorem Wbtw.wOppSide₁₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hy : y s) :
          s.WOppSide x z
          theorem Wbtw.wOppSide₃₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [StrictOrderedCommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Wbtw R x y z) (hy : y s) :
          s.WOppSide z x
          @[simp]
          theorem AffineSubspace.wOppSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} :
          s.WOppSide x x x s
          theorem AffineSubspace.not_sOppSide_self {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) :
          ¬s.SOppSide x x
          theorem AffineSubspace.wSameSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₁ : P} (h : p₁ s) :
          s.WSameSide x y x s p₂s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
          theorem AffineSubspace.wSameSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₂ : P} (h : p₂ s) :
          s.WSameSide x y y s p₁s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
          theorem AffineSubspace.sSameSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₁ : P} (h : p₁ s) :
          s.SSameSide x y xs ys p₂s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
          theorem AffineSubspace.sSameSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₂ : P} (h : p₂ s) :
          s.SSameSide x y xs ys p₁s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
          theorem AffineSubspace.wOppSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₁ : P} (h : p₁ s) :
          s.WOppSide x y x s p₂s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
          theorem AffineSubspace.wOppSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₂ : P} (h : p₂ s) :
          s.WOppSide x y y s p₁s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
          theorem AffineSubspace.sOppSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₁ : P} (h : p₁ s) :
          s.SOppSide x y xs ys p₂s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
          theorem AffineSubspace.sOppSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {p₂ : P} (h : p₂ s) :
          s.SOppSide x y xs ys p₁s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
          theorem AffineSubspace.WSameSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WSameSide x y) (hyz : s.WSameSide y z) (hy : ys) :
          s.WSameSide x z
          theorem AffineSubspace.WSameSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WSameSide x y) (hyz : s.SSameSide y z) :
          s.WSameSide x z
          theorem AffineSubspace.WSameSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WSameSide x y) (hyz : s.WOppSide y z) (hy : ys) :
          s.WOppSide x z
          theorem AffineSubspace.WSameSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WSameSide x y) (hyz : s.SOppSide y z) :
          s.WOppSide x z
          theorem AffineSubspace.SSameSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SSameSide x y) (hyz : s.WSameSide y z) :
          s.WSameSide x z
          theorem AffineSubspace.SSameSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SSameSide x y) (hyz : s.SSameSide y z) :
          s.SSameSide x z
          theorem AffineSubspace.SSameSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SSameSide x y) (hyz : s.WOppSide y z) :
          s.WOppSide x z
          theorem AffineSubspace.SSameSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SSameSide x y) (hyz : s.SOppSide y z) :
          s.SOppSide x z
          theorem AffineSubspace.WOppSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WOppSide x y) (hyz : s.WSameSide y z) (hy : ys) :
          s.WOppSide x z
          theorem AffineSubspace.WOppSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WOppSide x y) (hyz : s.SSameSide y z) :
          s.WOppSide x z
          theorem AffineSubspace.WOppSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WOppSide x y) (hyz : s.WOppSide y z) (hy : ys) :
          s.WSameSide x z
          theorem AffineSubspace.WOppSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.WOppSide x y) (hyz : s.SOppSide y z) :
          s.WSameSide x z
          theorem AffineSubspace.SOppSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SOppSide x y) (hyz : s.WSameSide y z) :
          s.WOppSide x z
          theorem AffineSubspace.SOppSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SOppSide x y) (hyz : s.SSameSide y z) :
          s.SOppSide x z
          theorem AffineSubspace.SOppSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SOppSide x y) (hyz : s.WOppSide y z) :
          s.WSameSide x z
          theorem AffineSubspace.SOppSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (hxy : s.SOppSide x y) (hyz : s.SOppSide y z) :
          s.SSameSide x z
          theorem AffineSubspace.wSameSide_and_wOppSide_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WSameSide x y s.WOppSide x y x s y s
          theorem AffineSubspace.WSameSide.not_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WSameSide x y) :
          ¬s.SOppSide x y
          theorem AffineSubspace.SSameSide.not_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          ¬s.WOppSide x y
          theorem AffineSubspace.SSameSide.not_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SSameSide x y) :
          ¬s.SOppSide x y
          theorem AffineSubspace.WOppSide.not_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.WOppSide x y) :
          ¬s.SSameSide x y
          theorem AffineSubspace.SOppSide.not_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          ¬s.WSameSide x y
          theorem AffineSubspace.SOppSide.not_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          ¬s.SSameSide x y
          theorem AffineSubspace.wOppSide_iff_exists_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} :
          s.WOppSide x y ps, Wbtw R x p y
          theorem AffineSubspace.SOppSide.exists_sbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (h : s.SOppSide x y) :
          ps, Sbtw R x p y
          theorem Sbtw.sOppSide_of_not_mem_of_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} {z : P} (h : Sbtw R x y z) (hx : xs) (hy : y s) :
          s.SOppSide x z
          theorem AffineSubspace.sSameSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p₁ : P} {p₂ : P} (hx : xs) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 < t) :
          s.SSameSide (t (x -ᵥ p₁) +ᵥ p₂) x
          theorem AffineSubspace.sSameSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p₁ : P} {p₂ : P} (hx : xs) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 < t) :
          s.SSameSide x (t (x -ᵥ p₁) +ᵥ p₂)
          theorem AffineSubspace.sSameSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (hx : x s) (hy : ys) {t : R} (ht : 0 < t) :
          s.SSameSide ((AffineMap.lineMap x y) t) y
          theorem AffineSubspace.sSameSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (hx : x s) (hy : ys) {t : R} (ht : 0 < t) :
          s.SSameSide y ((AffineMap.lineMap x y) t)
          theorem AffineSubspace.sOppSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p₁ : P} {p₂ : P} (hx : xs) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t < 0) :
          s.SOppSide (t (x -ᵥ p₁) +ᵥ p₂) x
          theorem AffineSubspace.sOppSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p₁ : P} {p₂ : P} (hx : xs) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t < 0) :
          s.SOppSide x (t (x -ᵥ p₁) +ᵥ p₂)
          theorem AffineSubspace.sOppSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (hx : x s) (hy : ys) {t : R} (ht : t < 0) :
          s.SOppSide ((AffineMap.lineMap x y) t) y
          theorem AffineSubspace.sOppSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (hx : x s) (hy : ys) {t : R} (ht : t < 0) :
          s.SOppSide y ((AffineMap.lineMap x y) t)
          theorem AffineSubspace.setOf_wSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p : P} (hx : xs) (hp : p s) :
          {y : P | s.WSameSide x y} = Set.image2 (fun (t : R) (q : P) => t (x -ᵥ p) +ᵥ q) (Set.Ici 0) s
          theorem AffineSubspace.setOf_sSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p : P} (hx : xs) (hp : p s) :
          {y : P | s.SSameSide x y} = Set.image2 (fun (t : R) (q : P) => t (x -ᵥ p) +ᵥ q) (Set.Ioi 0) s
          theorem AffineSubspace.setOf_wOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p : P} (hx : xs) (hp : p s) :
          {y : P | s.WOppSide x y} = Set.image2 (fun (t : R) (q : P) => t (x -ᵥ p) +ᵥ q) (Set.Iic 0) s
          theorem AffineSubspace.setOf_sOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {p : P} (hx : xs) (hp : p s) :
          {y : P | s.SOppSide x y} = Set.image2 (fun (t : R) (q : P) => t (x -ᵥ p) +ᵥ q) (Set.Iio 0) s
          theorem AffineSubspace.wOppSide_pointReflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x s) :
          s.WOppSide y ((AffineEquiv.pointReflection R x) y)
          theorem AffineSubspace.sOppSide_pointReflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [LinearOrderedField R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} {y : P} (hx : x s) (hy : ys) :
          s.SOppSide y ((AffineEquiv.pointReflection R x) y)
          theorem AffineSubspace.isConnected_setOf_wSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace P} (x : P) (h : (s).Nonempty) :
          IsConnected {y : P | s.WSameSide x y}
          theorem AffineSubspace.isConnected_setOf_sSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace P} {x : P} (hx : xs) (h : (s).Nonempty) :
          IsConnected {y : P | s.SSameSide x y}
          theorem AffineSubspace.isConnected_setOf_wOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace P} (x : P) (h : (s).Nonempty) :
          IsConnected {y : P | s.WOppSide x y}
          theorem AffineSubspace.isConnected_setOf_sOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace P} {x : P} (hx : xs) (h : (s).Nonempty) :
          IsConnected {y : P | s.SOppSide x y}