analysis.convex.segment

source

def segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x y : E) :

set E

Segments in a vector space.

Equations

segment 𝕜 x y = {z : E | ∃ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), a • x + b • y = z}

source

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.

Equations

open_segment 𝕜 x y = {z : E | ∃ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • x + b • y = z}

source

theorem segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (p : 𝕜 × 𝕜), p.fst • x + p.snd • y) '' {p : 𝕜 × 𝕜 | 0 ≤ p.fst ∧ 0 ≤ p.snd ∧ p.fst + p.snd = 1}

source

theorem open_segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (p : 𝕜 × 𝕜), p.fst • x + p.snd • y) '' {p : 𝕜 × 𝕜 | 0 < p.fst ∧ 0 < p.snd ∧ p.fst + p.snd = 1}

source

theorem segment_symm (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x y : E) :

segment 𝕜 x y = segment 𝕜 y x

source

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

source

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

source

theorem 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} :

segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

source

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} :

open_segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

source

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) :

x ∈ segment 𝕜 x y

source

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) :

y ∈ segment 𝕜 x y

source

@[simp]

theorem segment_same (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (x : E) :

segment 𝕜 x x = {x}

source

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

source

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

source

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

source

@[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}

source

theorem segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (θ : 𝕜), (1 - θ) • x + θ • y) '' set.Icc 0 1

source

theorem open_segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (θ : 𝕜), (1 - θ) • x + θ • y) '' set.Ioo 0 1

source

theorem segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (θ : 𝕜), x + θ • (y - x)) '' set.Icc 0 1

source

theorem open_segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (θ : 𝕜), x + θ • (y - x)) '' set.Ioo 0 1

source

theorem segment_eq_image_line_map (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = ⇑(affine_map.line_map x y) '' set.Icc 0 1

source

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

source

@[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) :

⇑f '' segment 𝕜 a b = segment 𝕜 (⇑f a) (⇑f b)

source

@[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)

source

@[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) :

a +ᵥ segment 𝕜 b c = segment 𝕜 (a +ᵥ b) (a +ᵥ c)

source

@[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)

source

@[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} :

a + x ∈ segment 𝕜 (a + b) (a + c) ↔ x ∈ segment 𝕜 b c

source

@[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

source

theorem 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) ⁻¹' segment 𝕜 (a + b) (a + c) = segment 𝕜 b c

source

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

source

theorem 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) '' segment 𝕜 b c = segment 𝕜 (a + b) (a + c)

source

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)

source

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) :

same_ray 𝕜 (x - y) (z - x)

source

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) :

midpoint 𝕜 x y ∈ segment 𝕜 x y

source

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) :

x ∈ segment 𝕜 (x - y) (x + y)

source

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) :

x ∈ segment 𝕜 (x + y) (x - y)

source

@[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

source

@[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

source

theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_semifield 𝕜] [add_comm_group E] [module 𝕜 E] {x y z : E} :

x ∈ segment 𝕜 y z ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

source

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} :

x ∈ open_segment 𝕜 y z ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

source

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} :

x ∈ segment 𝕜 y z ↔ same_ray 𝕜 (x - y) (z - x)

source

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).

source

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) :

segment 𝕜 x y ⊆ set.Icc x y

source

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

source

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) :

segment 𝕜 x y ⊆ set.uIcc x y

source

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

source

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

source

theorem Icc_subset_segment {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} :

set.Icc x y ⊆ segment 𝕜 x y

source

@[simp]

theorem segment_eq_Icc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x ≤ y) :

segment 𝕜 x y = set.Icc x y

source

theorem Ioo_subset_open_segment {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} :

set.Ioo x y ⊆ open_segment 𝕜 x y

source

@[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

source

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)

source

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)

source

theorem segment_eq_uIcc {𝕜 : Type u_1} [linear_ordered_field 𝕜] (x y : 𝕜) :

segment 𝕜 x y = set.uIcc x y

source

theorem convex.mem_Icc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y z : 𝕜} (h : x ≤ y) :

z ∈ set.Icc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Icc iff it can be expressed as a convex combination of the endpoints.

source

theorem convex.mem_Ioo {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y z : 𝕜} (h : x < y) :

z ∈ set.Ioo x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioo iff it can be expressed as a strict convex combination of the endpoints.

source

theorem convex.mem_Ioc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y z : 𝕜} (h : x < y) :

z ∈ set.Ioc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioc iff it can be expressed as a semistrict convex combination of the endpoints.

source

theorem convex.mem_Ico {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y z : 𝕜} (h : x < y) :

z ∈ set.Ico x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ico iff it can be expressed as a semistrict convex combination of the endpoints.

source

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) :

segment 𝕜 x y ⊆ segment 𝕜 x.fst y.fst ×ˢ segment 𝕜 x.snd y.snd

source

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

source

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) :

(λ (x : E), (x, y)) '' segment 𝕜 x₁ x₂ = segment 𝕜 (x₁, y) (x₂, y)

source

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) :

(λ (y : F), (x, y)) '' segment 𝕜 y₁ y₂ = segment 𝕜 (x, y₁) (x, y₂)

source

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)

source

@[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₂)

source

theorem pi.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) :

segment 𝕜 x y ⊆ s.pi (λ (i : ι), segment 𝕜 (x i) (y i))

source

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))

source

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₂)

source

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₂)

mathlib documentation

Segments in vector spaces #

Notations #

TODO #

Segments in an ordered space #