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
open_segment_subset_iff
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E}
{x y : E} :
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
theorem
segment_image
(π : 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
open_segment_image
(π : 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)
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}
[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_open_segment_iff_div
{π : Type u_1}
{E : Type u_2}
[linear_ordered_semifield π]
[add_comm_group E]
[module π E]
{x y z : E} :
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
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_interval
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
(x y : E) :
segment π x y β set.interval x y
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
segment_eq_interval
{π : Type u_1}
[linear_ordered_field π]
(x y : π) :
segment π x y = set.interval x y