mathlib3 documentation

analysis.convex.side

Sides of affine subspaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

def affine_subspace.w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (s : affine_subspace R P) (x y : P) :
Prop

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

Equations
def affine_subspace.s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (s : affine_subspace R P) (x y : P) :
Prop

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

Equations
def affine_subspace.w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (s : affine_subspace R P) (x y : P) :
Prop

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

Equations
def affine_subspace.s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (s : affine_subspace R P) (x y : P) :
Prop

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

Equations
theorem affine_subspace.w_same_side.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (h : s.w_same_side x y) (f : P →ᵃ[R] P') :
theorem function.injective.w_same_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : function.injective f) :
theorem function.injective.s_same_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : function.injective f) :
@[simp]
theorem affine_equiv.w_same_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (f : P ≃ᵃ[R] P') :
@[simp]
theorem affine_equiv.s_same_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (f : P ≃ᵃ[R] P') :
theorem affine_subspace.w_opp_side.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (h : s.w_opp_side x y) (f : P →ᵃ[R] P') :
theorem function.injective.w_opp_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : function.injective f) :
theorem function.injective.s_opp_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : function.injective f) :
@[simp]
theorem affine_equiv.w_opp_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (f : P ≃ᵃ[R] P') :
@[simp]
theorem affine_equiv.s_opp_side_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] [add_comm_group V'] [module R V'] [add_torsor V' P'] {s : affine_subspace R P} {x y : P} (f : P ≃ᵃ[R] P') :
theorem affine_subspace.w_same_side.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.w_same_side x y) :
theorem affine_subspace.s_same_side.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
theorem affine_subspace.w_opp_side.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.w_opp_side x y) :
theorem affine_subspace.s_opp_side.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
theorem affine_subspace.s_same_side.w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
theorem affine_subspace.s_same_side.left_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
x s
theorem affine_subspace.s_same_side.right_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
y s
theorem affine_subspace.s_opp_side.w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
theorem affine_subspace.s_opp_side.left_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
x s
theorem affine_subspace.s_opp_side.right_not_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
y s
theorem affine_subspace.w_same_side_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
theorem affine_subspace.w_same_side.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :

Alias of the forward direction of affine_subspace.w_same_side_comm.

theorem affine_subspace.s_same_side_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
theorem affine_subspace.s_same_side.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :

Alias of the forward direction of affine_subspace.s_same_side_comm.

theorem affine_subspace.w_opp_side_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
theorem affine_subspace.w_opp_side.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :

Alias of the forward direction of affine_subspace.w_opp_side_comm.

theorem affine_subspace.s_opp_side_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
theorem affine_subspace.s_opp_side.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :

Alias of the forward direction of affine_subspace.s_opp_side_comm.

theorem affine_subspace.not_w_same_side_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
theorem affine_subspace.not_s_same_side_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
theorem affine_subspace.not_w_opp_side_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
theorem affine_subspace.not_s_opp_side_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] (x y : P) :
@[simp]
theorem affine_subspace.w_same_side_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} :
theorem affine_subspace.s_same_side_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} :
theorem affine_subspace.w_same_side_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (hx : x s) :
theorem affine_subspace.w_same_side_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} (x : P) {y : P} (hy : y s) :
theorem affine_subspace.w_opp_side_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (hx : x s) :
theorem affine_subspace.w_opp_side_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} (x : P) {y : P} (hy : y s) :
theorem affine_subspace.w_same_side_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
theorem affine_subspace.w_same_side_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
theorem affine_subspace.s_same_side_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
theorem affine_subspace.s_same_side_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
theorem affine_subspace.w_opp_side_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
s.w_opp_side (v +ᵥ x) y s.w_opp_side x y
theorem affine_subspace.w_opp_side_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
s.w_opp_side x (v +ᵥ y) s.w_opp_side x y
theorem affine_subspace.s_opp_side_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
s.s_opp_side (v +ᵥ x) y s.s_opp_side x y
theorem affine_subspace.s_opp_side_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} {v : V} (hv : v s.direction) :
s.s_opp_side x (v +ᵥ y) s.s_opp_side x y
theorem affine_subspace.w_same_side_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 t) :
s.w_same_side (t (x -ᵥ p₁) +ᵥ p₂) x
theorem affine_subspace.w_same_side_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 t) :
s.w_same_side x (t (x -ᵥ p₁) +ᵥ p₂)
theorem affine_subspace.w_same_side_line_map_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : 0 t) :
theorem affine_subspace.w_same_side_line_map_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : 0 t) :
theorem affine_subspace.w_opp_side_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t 0) :
s.w_opp_side (t (x -ᵥ p₁) +ᵥ p₂) x
theorem affine_subspace.w_opp_side_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t 0) :
s.w_opp_side x (t (x -ᵥ p₁) +ᵥ p₂)
theorem affine_subspace.w_opp_side_line_map_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : t 0) :
theorem affine_subspace.w_opp_side_line_map_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (h : x s) {t : R} (ht : t 0) :
theorem wbtw.w_same_side₂₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hx : x s) :
theorem wbtw.w_same_side₃₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hx : x s) :
theorem wbtw.w_same_side₁₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hz : z s) :
theorem wbtw.w_same_side₂₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hz : z s) :
theorem wbtw.w_opp_side₁₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hy : y s) :
theorem wbtw.w_opp_side₃₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [strict_ordered_comm_ring R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : wbtw R x y z) (hy : y s) :
@[simp]
theorem affine_subspace.w_opp_side_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} :
s.w_opp_side x x x s
theorem affine_subspace.not_s_opp_side_self {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] (s : affine_subspace R P) (x : P) :
theorem affine_subspace.w_same_side_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₁ : P} (h : p₁ s) :
s.w_same_side x y x s (p₂ : P) (H : p₂ s), same_ray R (x -ᵥ p₁) (y -ᵥ p₂)
theorem affine_subspace.w_same_side_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₂ : P} (h : p₂ s) :
s.w_same_side x y y s (p₁ : P) (H : p₁ s), same_ray R (x -ᵥ p₁) (y -ᵥ p₂)
theorem affine_subspace.s_same_side_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₁ : P} (h : p₁ s) :
s.s_same_side x y x s y s (p₂ : P) (H : p₂ s), same_ray R (x -ᵥ p₁) (y -ᵥ p₂)
theorem affine_subspace.s_same_side_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₂ : P} (h : p₂ s) :
s.s_same_side x y x s y s (p₁ : P) (H : p₁ s), same_ray R (x -ᵥ p₁) (y -ᵥ p₂)
theorem affine_subspace.w_opp_side_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₁ : P} (h : p₁ s) :
s.w_opp_side x y x s (p₂ : P) (H : p₂ s), same_ray R (x -ᵥ p₁) (p₂ -ᵥ y)
theorem affine_subspace.w_opp_side_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₂ : P} (h : p₂ s) :
s.w_opp_side x y y s (p₁ : P) (H : p₁ s), same_ray R (x -ᵥ p₁) (p₂ -ᵥ y)
theorem affine_subspace.s_opp_side_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₁ : P} (h : p₁ s) :
s.s_opp_side x y x s y s (p₂ : P) (H : p₂ s), same_ray R (x -ᵥ p₁) (p₂ -ᵥ y)
theorem affine_subspace.s_opp_side_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y p₂ : P} (h : p₂ s) :
s.s_opp_side x y x s y s (p₁ : P) (H : p₁ s), same_ray R (x -ᵥ p₁) (p₂ -ᵥ y)
theorem affine_subspace.w_same_side.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_same_side x y) (hyz : s.w_same_side y z) (hy : y s) :
theorem affine_subspace.w_same_side.trans_s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_same_side x y) (hyz : s.s_same_side y z) :
theorem affine_subspace.w_same_side.trans_w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_same_side x y) (hyz : s.w_opp_side y z) (hy : y s) :
theorem affine_subspace.w_same_side.trans_s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_same_side x y) (hyz : s.s_opp_side y z) :
theorem affine_subspace.s_same_side.trans_w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_same_side x y) (hyz : s.w_same_side y z) :
theorem affine_subspace.s_same_side.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_same_side x y) (hyz : s.s_same_side y z) :
theorem affine_subspace.s_same_side.trans_w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_same_side x y) (hyz : s.w_opp_side y z) :
theorem affine_subspace.s_same_side.trans_s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_same_side x y) (hyz : s.s_opp_side y z) :
theorem affine_subspace.w_opp_side.trans_w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_opp_side x y) (hyz : s.w_same_side y z) (hy : y s) :
theorem affine_subspace.w_opp_side.trans_s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_opp_side x y) (hyz : s.s_same_side y z) :
theorem affine_subspace.w_opp_side.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_opp_side x y) (hyz : s.w_opp_side y z) (hy : y s) :
theorem affine_subspace.w_opp_side.trans_s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.w_opp_side x y) (hyz : s.s_opp_side y z) :
theorem affine_subspace.s_opp_side.trans_w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_opp_side x y) (hyz : s.w_same_side y z) :
theorem affine_subspace.s_opp_side.trans_s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_opp_side x y) (hyz : s.s_same_side y z) :
theorem affine_subspace.s_opp_side.trans_w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_opp_side x y) (hyz : s.w_opp_side y z) :
theorem affine_subspace.s_opp_side.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (hxy : s.s_opp_side x y) (hyz : s.s_opp_side y z) :
theorem affine_subspace.w_same_side_and_w_opp_side_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
s.w_same_side x y s.w_opp_side x y x s y s
theorem affine_subspace.w_same_side.not_s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.w_same_side x y) :
theorem affine_subspace.s_same_side.not_w_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
theorem affine_subspace.s_same_side.not_s_opp_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_same_side x y) :
theorem affine_subspace.w_opp_side.not_s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.w_opp_side x y) :
theorem affine_subspace.s_opp_side.not_w_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
theorem affine_subspace.s_opp_side.not_s_same_side {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
theorem affine_subspace.w_opp_side_iff_exists_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} :
s.w_opp_side x y (p : P) (H : p s), wbtw R x p y
theorem affine_subspace.s_opp_side.exists_sbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (h : s.s_opp_side x y) :
(p : P) (H : p s), sbtw R x p y
theorem sbtw.s_opp_side_of_not_mem_of_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y z : P} (h : sbtw R x y z) (hx : x s) (hy : y s) :
theorem affine_subspace.s_same_side_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p₁ p₂ : P} (hx : x s) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 < t) :
s.s_same_side (t (x -ᵥ p₁) +ᵥ p₂) x
theorem affine_subspace.s_same_side_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p₁ p₂ : P} (hx : x s) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : 0 < t) :
s.s_same_side x (t (x -ᵥ p₁) +ᵥ p₂)
theorem affine_subspace.s_same_side_line_map_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (hx : x s) (hy : y s) {t : R} (ht : 0 < t) :
theorem affine_subspace.s_same_side_line_map_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (hx : x s) (hy : y s) {t : R} (ht : 0 < t) :
theorem affine_subspace.s_opp_side_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p₁ p₂ : P} (hx : x s) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t < 0) :
s.s_opp_side (t (x -ᵥ p₁) +ᵥ p₂) x
theorem affine_subspace.s_opp_side_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p₁ p₂ : P} (hx : x s) (hp₁ : p₁ s) (hp₂ : p₂ s) {t : R} (ht : t < 0) :
s.s_opp_side x (t (x -ᵥ p₁) +ᵥ p₂)
theorem affine_subspace.s_opp_side_line_map_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (hx : x s) (hy : y s) {t : R} (ht : t < 0) :
theorem affine_subspace.s_opp_side_line_map_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (hx : x s) (hy : y s) {t : R} (ht : t < 0) :
theorem affine_subspace.set_of_w_same_side_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p : P} (hx : x s) (hp : p s) :
{y : P | s.w_same_side x y} = set.image2 (λ (t : R) (q : P), t (x -ᵥ p) +ᵥ q) (set.Ici 0) s
theorem affine_subspace.set_of_s_same_side_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p : P} (hx : x s) (hp : p s) :
{y : P | s.s_same_side x y} = set.image2 (λ (t : R) (q : P), t (x -ᵥ p) +ᵥ q) (set.Ioi 0) s
theorem affine_subspace.set_of_w_opp_side_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p : P} (hx : x s) (hp : p s) :
{y : P | s.w_opp_side x y} = set.image2 (λ (t : R) (q : P), t (x -ᵥ p) +ᵥ q) (set.Iic 0) s
theorem affine_subspace.set_of_s_opp_side_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x p : P} (hx : x s) (hp : p s) :
{y : P | s.s_opp_side x y} = set.image2 (λ (t : R) (q : P), t (x -ᵥ p) +ᵥ q) (set.Iio 0) s
theorem affine_subspace.w_opp_side_point_reflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x : P} (y : P) (hx : x s) :
theorem affine_subspace.s_opp_side_point_reflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [linear_ordered_field R] [add_comm_group V] [module R V] [add_torsor V P] {s : affine_subspace R P} {x y : P} (hx : x s) (hy : y s) :