Segments in vector spaces #
In a π-vector space, we define the following objects and properties.
segment π x y
: Closed segment joiningx
andy
.open_segment π x y
: Open segment joiningx
andy
.
Notations #
We provide the following notation:
TODO #
Generalize all this file to affine spaces.
Should we rename segment
and open_segment
to convex.Icc
and convex.Ioo
? Should we also
define clopen_segment
/convex.Ico
/convex.Ioc
?
def
open_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
(x y : E) :
set E
Open segment in a vector space. Note that open_segment π x x = {x}
instead of being β
when
the base semiring has some element between 0
and 1
.
theorem
segment_symm
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
(x y : E) :
theorem
open_segment_symm
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
(x y : E) :
open_segment π x y = open_segment π y x
theorem
open_segment_subset_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
(x y : E) :
open_segment π x y β segment π x y
theorem
left_mem_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[mul_action_with_zero π E]
(x y : E) :
theorem
right_mem_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[mul_action_with_zero π E]
(x y : E) :
@[simp]
theorem
segment_same
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(x : E) :
theorem
insert_endpoints_open_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(x y : E) :
has_insert.insert x (has_insert.insert y (open_segment π x y)) = segment π x y
theorem
mem_open_segment_of_ne_left_right
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{x y z : E}
(hx : x β z)
(hy : y β z)
(hz : z β segment π x y) :
z β open_segment π x y
theorem
open_segment_subset_iff_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
{x y : E}
(hx : x β s)
(hy : y β s) :
open_segment π x y β s β segment π x y β s
@[simp]
theorem
open_segment_same
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
[nontrivial π]
[densely_ordered π]
(x : E) :
open_segment π x x = {x}
theorem
segment_eq_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
open_segment_eq_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
segment_eq_image'
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
open_segment_eq_image'
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
segment_eq_image_line_map
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
open_segment_eq_image_line_map
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
open_segment π x y = β(affine_map.line_map x y) '' set.Ioo 0 1
@[simp]
theorem
image_segment
(π : Type u_1)
{E : Type u_2}
{F : Type u_3}
[ordered_ring π]
[add_comm_group E]
[add_comm_group F]
[module π E]
[module π F]
(f : E βα΅[π] F)
(a b : E) :
@[simp]
theorem
image_open_segment
(π : Type u_1)
{E : Type u_2}
{F : Type u_3}
[ordered_ring π]
[add_comm_group E]
[add_comm_group F]
[module π E]
[module π F]
(f : E βα΅[π] F)
(a b : E) :
βf '' open_segment π a b = open_segment π (βf a) (βf b)
@[simp]
theorem
vadd_segment
(π : Type u_1)
{E : Type u_2}
{G : Type u_4}
[ordered_ring π]
[add_comm_group E]
[add_comm_group G]
[module π E]
[add_torsor G E]
[vadd_comm_class G E E]
(a : G)
(b c : E) :
@[simp]
theorem
vadd_open_segment
(π : Type u_1)
{E : Type u_2}
{G : Type u_4}
[ordered_ring π]
[add_comm_group E]
[add_comm_group G]
[module π E]
[add_torsor G E]
[vadd_comm_class G E E]
(a : G)
(b c : E) :
a +α΅₯ open_segment π b c = open_segment π (a +α΅₯ b) (a +α΅₯ c)
@[simp]
theorem
mem_segment_translate
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a : E)
{x b c : E} :
@[simp]
theorem
mem_open_segment_translate
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a : E)
{x b c : E} :
a + x β open_segment π (a + b) (a + c) β x β open_segment π b c
theorem
segment_translate_preimage
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
theorem
open_segment_translate_preimage
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
(Ξ» (x : E), a + x) β»ΒΉ' open_segment π (a + b) (a + c) = open_segment π b c
theorem
segment_translate_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
theorem
open_segment_translate_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
(Ξ» (x : E), a + x) '' open_segment π b c = open_segment π (a + b) (a + c)
theorem
same_ray_of_mem_segment
{π : Type u_1}
{E : Type u_2}
[strict_ordered_comm_ring π]
[add_comm_group E]
[module π E]
{x y z : E}
(h : x β segment π y z) :
theorem
midpoint_mem_segment
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
theorem
mem_segment_sub_add
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
theorem
mem_segment_add_sub
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
@[simp]
theorem
left_mem_open_segment_iff
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
{x y : E}
[densely_ordered π]
[no_zero_smul_divisors π E] :
x β open_segment π x y β x = y
@[simp]
theorem
right_mem_open_segment_iff
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
{x y : E}
[densely_ordered π]
[no_zero_smul_divisors π E] :
y β open_segment π x y β x = y
theorem
mem_segment_iff_same_ray
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{x y z : E} :
theorem
open_segment_subset_union
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
(x y : E)
{z : E}
(hz : z β set.range β(affine_map.line_map x y)) :
open_segment π x y β has_insert.insert z (open_segment π x z βͺ open_segment π z y)
If z = line_map x y c
is a point on the line passing through x
and y
, then the open
segment open_segment π x y
is included in the union of the open segments open_segment π x z
,
open_segment π z y
, and the point z
. Informally, (x, y) β {z} βͺ (x, z) βͺ (z, y)
.
theorem
segment_subset_Icc
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{x y : E}
(h : x β€ y) :
theorem
open_segment_subset_Ioo
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{x y : E}
(h : x < y) :
open_segment π x y β set.Ioo x y
theorem
segment_subset_uIcc
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
(x y : E) :
theorem
convex.min_le_combo
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{a b : π}
(x y : E)
(ha : 0 β€ a)
(hb : 0 β€ b)
(hab : a + b = 1) :
linear_order.min x y β€ a β’ x + b β’ y
theorem
convex.combo_le_max
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{a b : π}
(x y : E)
(ha : 0 β€ a)
(hb : 0 β€ b)
(hab : a + b = 1) :
a β’ x + b β’ y β€ linear_order.max x y
@[simp]
theorem
Ioo_subset_open_segment
{π : Type u_1}
[linear_ordered_field π]
{x y : π} :
set.Ioo x y β open_segment π x y
@[simp]
theorem
open_segment_eq_Ioo
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(h : x < y) :
open_segment π x y = set.Ioo x y
theorem
segment_eq_Icc'
{π : Type u_1}
[linear_ordered_field π]
(x y : π) :
segment π x y = set.Icc (linear_order.min x y) (linear_order.max x y)
theorem
open_segment_eq_Ioo'
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(hxy : x β y) :
open_segment π x y = set.Ioo (linear_order.min x y) (linear_order.max x y)
theorem
prod.segment_subset
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(x y : E Γ F) :
theorem
prod.open_segment_subset
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(x y : E Γ F) :
open_segment π x y β open_segment π x.fst y.fst ΓΛ’ open_segment π x.snd y.snd
theorem
prod.image_mk_segment_left
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(xβ xβ : E)
(y : F) :
theorem
prod.image_mk_segment_right
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(x : E)
(yβ yβ : F) :
theorem
prod.image_mk_open_segment_left
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(xβ xβ : E)
(y : F) :
(Ξ» (x : E), (x, y)) '' open_segment π xβ xβ = open_segment π (xβ, y) (xβ, y)
@[simp]
theorem
prod.image_mk_open_segment_right
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
(x : E)
(yβ yβ : F) :
(Ξ» (y : F), (x, y)) '' open_segment π yβ yβ = open_segment π (x, yβ) (x, yβ)
theorem
pi.open_segment_subset
{π : Type u_1}
{ΞΉ : Type u_5}
{Ο : ΞΉ β Type u_6}
[ordered_semiring π]
[Ξ (i : ΞΉ), add_comm_monoid (Ο i)]
[Ξ (i : ΞΉ), module π (Ο i)]
{s : set ΞΉ}
(x y : Ξ (i : ΞΉ), Ο i) :
open_segment π x y β s.pi (Ξ» (i : ΞΉ), open_segment π (x i) (y i))
theorem
pi.image_update_segment
{π : Type u_1}
{ΞΉ : Type u_5}
{Ο : ΞΉ β Type u_6}
[ordered_semiring π]
[Ξ (i : ΞΉ), add_comm_monoid (Ο i)]
[Ξ (i : ΞΉ), module π (Ο i)]
[decidable_eq ΞΉ]
(i : ΞΉ)
(xβ xβ : Ο i)
(y : Ξ (i : ΞΉ), Ο i) :
function.update y i '' segment π xβ xβ = segment π (function.update y i xβ) (function.update y i xβ)
theorem
pi.image_update_open_segment
{π : Type u_1}
{ΞΉ : Type u_5}
{Ο : ΞΉ β Type u_6}
[ordered_semiring π]
[Ξ (i : ΞΉ), add_comm_monoid (Ο i)]
[Ξ (i : ΞΉ), module π (Ο i)]
[decidable_eq ΞΉ]
(i : ΞΉ)
(xβ xβ : Ο i)
(y : Ξ (i : ΞΉ), Ο i) :
function.update y i '' open_segment π xβ xβ = open_segment π (function.update y i xβ) (function.update y i xβ)