General

theorem SplitProperties.firstPart_cast {X : Type u} [DirectedSpace X] {x₀ x₁ x₀' x₁' : X} (γ : Dipath x₀ x₁) (hx₀ : x₀' = x₀) (hx₁ : x₁' = x₁) (T : ↑unitInterval) : SplitDipath.FirstPart (γ.cast hx₀ hx₁) T = (SplitDipath.FirstPart γ T).cast hx₀ ⋯

theorem SplitProperties.secondPart_cast {X : Type u} [DirectedSpace X] {x₀ x₁ x₀' x₁' : X} (γ : Dipath x₀ x₁) (hx₀ : x₀' = x₀) (hx₁ : x₁' = x₁) (T : ↑unitInterval) : SplitDipath.SecondPart (γ.cast hx₀ hx₁) T = (SplitDipath.SecondPart γ T).cast ⋯ hx₁

theorem SplitProperties.firstPart_eq_of_split_point_eq {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {T T' : ↑unitInterval} (hT : T = T') : SplitDipath.FirstPart γ T = (SplitDipath.FirstPart γ T').cast ⋯ ⋯

theorem SplitProperties.secondPart_eq_of_split_point_eq {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {T T' : ↑unitInterval} (hT : T = T') : SplitDipath.SecondPart γ T = (SplitDipath.SecondPart γ T').cast ⋯ ⋯

theorem SplitProperties.firstPart_eq_of_point_eq {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {T T' : ↑unitInterval} (h : T = T') (t : ↑unitInterval) : (SplitDipath.FirstPart γ T) t = (SplitDipath.FirstPart γ T') t

theorem SplitProperties.secondPart_eq_of_point_eq {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {T T' : ↑unitInterval} (h : T = T') (t : ↑unitInterval) : (SplitDipath.SecondPart γ T) t = (SplitDipath.SecondPart γ T') t

theorem SplitProperties.interval_cast {X : Type u} [DirectedSpace X] {x₀ x₁ : X} {γ : Dipath x₀ x₁} {A : Set X} {a b a' b' : ↑unitInterval} (h_im : A = ⇑γ '' Set.Icc a b) (ha : a' = a) (hb : b' = b) : A = ⇑γ '' Set.Icc a' b'

First Part

theorem SplitProperties.firstPart_image {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T a b : ↑unitInterval) (h_ab : a ≤ b) : ⇑(SplitDipath.FirstPart γ T) '' Set.Icc a b = ⇑γ '' Set.Icc (T * a) (T * b)

theorem SplitProperties.firstPart_range {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T : ↑unitInterval) : Set.range ⇑(SplitDipath.FirstPart γ T) = ⇑γ '' Set.Icc 0 T

theorem SplitProperties.firstPart_range_interval {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n : ℕ} (h : 0 < n) : Set.range ⇑(SplitDipath.FirstPart γ (Fraction.ofPos h)) = ⇑γ '' Set.Icc 0 (Fraction.ofPos h)

theorem SplitProperties.firstPart_range_interval_coe {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n : ℕ} (h : 0 < n) : Set.range ⇑(SplitDipath.FirstPart γ (Fraction.ofPos h)) = ⇑γ.extend '' Set.Icc 0 (1 / ↑n)

theorem SplitProperties.firstPart_range_interval_partial {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n d i : ℕ} (hd : d.succ < n.succ) (hi : i < d.succ) : ⇑(SplitDipath.FirstPart γ (Fraction ⋯ ⋯)) '' Set.Icc (Fraction ⋯ ⋯) (Fraction ⋯ ⋯) = ⇑γ '' Set.Icc (Fraction ⋯ ⋯) (Fraction ⋯ ⋯)

If γ is a path, then the image of [i/(d+1), (i+1)/(d+1)] under γ split at (d+1)/(n+1) is the image of [i/(n+1), (i+1)/(n+1)] under γ

theorem SplitProperties.firstPart_range_interval_partial_coe {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n d i : ℕ} (hd : d.succ < n.succ) (hi : i < d.succ) : ⇑(SplitDipath.FirstPart γ (Fraction ⋯ ⋯)).extend '' Set.Icc (↑i / (↑d + 1)) ((↑i + 1) / (↑d + 1)) = ⇑γ.extend '' Set.Icc (↑i / (↑n + 1)) ((↑i + 1) / (↑n + 1))

If γ is a path, then the image of [i/(d+1), (i+1)/(d+1)] under γ split at (d+1)/(n+1) is the image of [i/(n+1), (i+1)/(n+1)] under γ.

Second Part

theorem SplitProperties.secondPart_image {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T a b : ↑unitInterval) (h_ab : a ≤ b) : ⇑(SplitDipath.SecondPart γ T) '' Set.Icc a b = ⇑γ '' Set.Icc ⟨↑(unitInterval.symm T) * ↑a + ↑T, ⋯⟩ ⟨↑(unitInterval.symm T) * ↑b + ↑T, ⋯⟩

theorem SplitProperties.secondPart_range {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T : ↑unitInterval) : Set.range ⇑(SplitDipath.SecondPart γ T) = ⇑γ '' Set.Icc T 1

theorem SplitProperties.secondPart_range_interval {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {i n : ℕ} (hi : i < n) (hn : 0 < n) : ⇑(SplitDipath.SecondPart γ (Fraction.ofPos ⋯)) '' Set.Icc (Fraction hn ⋯) (Fraction hn ⋯) = ⇑γ '' Set.Icc (Fraction ⋯ ⋯) (Fraction ⋯ ⋯)

When γ is a dipath, an we split it on the intervals [0, 1/(n+1)] and [1/(n+1), 1], then the image of γ of [(i+1)/(n+1), (i+2)/(n+1)] is equal to the image the second part of γ of [i/n, (i+1)/n]

theorem SplitProperties.secondPart_range_interval_coe {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {i n : ℕ} (hi : i < n) (hn : 0 < n) : ⇑(SplitDipath.SecondPart γ (Fraction.ofPos ⋯)).extend '' Set.Icc (↑i / ↑n) ((↑i + 1) / ↑n) = ⇑γ.extend '' Set.Icc ((↑i + 1) / (↑n + 1)) ((↑i + 1 + 1) / (↑n + 1))

When γ is a dipath, an we split it on the intervals [0, 1/(n+1)] and [1/(n+1), 1], then the image of γ of [(i+1)/(n+1), (i+2)/(n+1)] is equal to the image the second part of γ of [i/n, (i+1)/n]. Version with interval of real numbers

theorem SplitProperties.secondPart_range_partial_interval {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {i d n : ℕ} (hd : d.succ < n.succ) (hi : i < n - d) : ⇑(SplitDipath.SecondPart γ (Fraction ⋯ ⋯)) '' Set.Icc (Fraction ⋯ ⋯) (Fraction ⋯ ⋯) = ⇑γ '' Set.Icc (Fraction ⋯ ⋯) (Fraction ⋯ ⋯)

When γ is a dipath, an we split it on the intervals [0, (d+1)/(n+1)] and [(d+1)/(n+1), 1], then the image of γ of [(i+d.succ)/(n+1), (i+d.succ+1)/(n+1)] is equal to the image the second part of γ of [(i/(n-d), (i+1)/(n-d)].

theorem SplitProperties.secondPart_range_partial_interval_coe {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {i d n : ℕ} (hd : d.succ < n.succ) (hi : i < n - d) : ⇑(SplitDipath.SecondPart γ (Fraction ⋯ ⋯)).extend '' Set.Icc (↑i / (↑n - ↑d)) ((↑i + 1) / (↑n - ↑d)) = ⇑γ.extend '' Set.Icc (↑(i + d.succ) / (↑n + 1)) ((↑(i + d.succ) + 1) / (↑n + 1))

When γ is a dipath, an we split it on the intervals [0, (d+1)/(n+1)] and [(d+1)/(n+1), 1], then the image of γ of [(i+d.succ)/(n+1), (i+d.succ+1)/(n+1)] is equal to the image the second part of γ of [i/(n-d), (i+1)/(n-d)].

Mixed Parts

theorem SplitProperties.firstPart_of_firstPart {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n k : ℕ} (hkn : k < n) (hk : 0 < k) : SplitDipath.FirstPart (SplitDipath.FirstPart γ (Fraction ⋯ ⋯)) (Fraction.ofPos hk) = (SplitDipath.FirstPart γ (Fraction.ofPos ⋯)).cast ⋯ ⋯

Splitting a dipath γ at [0, k/n] and then at [0, 1/k] is the same as splitting it at [0, 1/n].

theorem SplitProperties.first_part_of_second_part {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n k : ℕ} (hkn : k < n) (hk : 0 < k) : SplitDipath.SecondPart (SplitDipath.FirstPart γ (Fraction ⋯ ⋯)) (Fraction.ofPos ⋯) = (SplitDipath.FirstPart (SplitDipath.SecondPart γ (Fraction.ofPos ⋯)) (Fraction ⋯ ⋯)).cast ⋯ ⋯

Splitting a dipath [0, (k+1)/(n+1)] and then [1/(k+1), 1] is the same as splitting it [1/(n+1), 1] and then [0, k/n]

theorem SplitProperties.second_part_of_second_part {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {n k : ℕ} (hkn : k < n) : SplitDipath.SecondPart (SplitDipath.SecondPart γ (Fraction.ofPos ⋯)) (Fraction ⋯ ⋯) = (SplitDipath.SecondPart γ (Fraction ⋯ ⋯)).cast ⋯ ⋯

Splitting a dipath [(k+2)/(n+2), 1] is the same as splitting it [1/(n+2), 1] and then [(k+1)/(n+1), 1]

Trans Parts

theorem SplitProperties.first_part_trans {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) : SplitDipath.FirstPart (γ₁.trans γ₂) (Fraction.ofPos ⋯) = γ₁.cast ⋯ ⋯

If γ₁ and γ₂ are two paths, then the first part of γ₁.trans γ₂ split at 1/2 is γ₁

theorem SplitProperties.second_part_trans {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) : SplitDipath.SecondPart (γ₁.trans γ₂) (Fraction.ofPos ⋯) = γ₂.cast ⋯ ⋯

If γ₁ and γ₂ are two paths, then the second part of γ₁.trans γ₂ split at 1/2 is γ₂

theorem SplitProperties.trans_first_part {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) (n : ℕ) (t : ↑unitInterval) : (SplitDipath.FirstPart (γ₁.trans γ₂) (Fraction.ofPos ⋯)) t = (SplitDipath.FirstPart γ₁ (Fraction.ofPos ⋯)) t

If γ₁ and γ₂ are two paths, then the first part of γ₁.trans γ₂ split at 1/(2n + 2) is the same as γ₁ split at 1/(n + 1).

theorem SplitProperties.AuxEqualities.h₁ (t : ↑unitInterval) : 0 ≤ ↑t

theorem SplitProperties.AuxEqualities.h₂ (n : ℕ) : 0 ≤ ↑n

theorem SplitProperties.AuxEqualities.h₃ (n : ℕ) : ↑n + 1 + 1 ≠ 0

theorem SplitProperties.AuxEqualities.h₄ (n : ℕ) : ↑n + ↑n + 1 + 1 + 1 + 1 > 0

theorem SplitProperties.AuxEqualities.h₅ (n : ℕ) : ↑n + ↑n + 1 + 1 + 1 + 1 = 2 * (↑n + 1 + 1)

theorem SplitProperties.AuxEqualities.h₆ (n : ℕ) : (↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1 + 1) = 2⁻¹

theorem SplitProperties.AuxEqualities.h₇ (n : ℕ) : ↑n + ↑n + 1 + 1 + 1 ≠ 0

theorem SplitProperties.AuxEqualities.h₈ (n : ℕ) : ↑n + 1 + (↑n + 1) + 1 + 1 = ↑n + ↑n + 1 + 1 + 1 + 1

theorem SplitProperties.AuxEqualities.e₁ (n : ℕ) (t : ↑unitInterval) : (1 - (↑n + 1) / (↑n + 1 + 1)) * ↑t + (↑n + 1) / (↑n + 1 + 1) = (↑t + ↑n + 1) / (↑n + 1 + 1)

theorem SplitProperties.AuxEqualities.e₂ (n : ℕ) (t : ↑unitInterval) : (1 - (↑n + ↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1)) * ↑t + (↑n + ↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1) = (↑t + ↑n + ↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1)

theorem SplitProperties.AuxEqualities.e₃ (n : ℕ) : 1 - (↑n + 1 + (↑n + 1) + 1 + 1)⁻¹ = (↑n + ↑n + 1 + 1 + 1) / (↑n + ↑n + 1 + 1 + 1 + 1)

theorem SplitProperties.AuxEqualities.e₄ (n : ℕ) (t : ↑unitInterval) : (↑n + ↑n + 1 + 1 + 1) / (↑n + ↑n + 1 + 1 + 1 + 1) * ((↑t + ↑n + ↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1)) = (↑t + ↑n + ↑n + 1 + 1) / (↑n + ↑n + 1 + 1 + 1 + 1)

theorem SplitProperties.AuxEqualities.e₅ (n : ℕ) (r : ℝ) : 2 * (r / (↑n + ↑n + 1 + 1 + 1 + 1) + (↑n + 1 + (↑n + 1) + 1 + 1)⁻¹) = (r + 1) / (↑n + 1 + 1)

theorem SplitProperties.AuxEqualities.e₆ (n : ℕ) (r : ℝ) : (1 - (↑n + 1 + 1)⁻¹) * r + (↑n + 1 + 1)⁻¹ = ((↑n + 1) * r + 1) / (↑n + 1 + 1)

theorem SplitProperties.trans_first_part_of_second_part {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) (n : ℕ) (t : ↑unitInterval) : (SplitDipath.FirstPart (SplitDipath.SecondPart (γ₁.trans γ₂) (Fraction.ofPos ⋯)) (Fraction ⋯ ⋯)) t = ((SplitDipath.SecondPart γ₁ (Fraction.ofPos ⋯)).trans (SplitDipath.FirstPart γ₂ (Fraction ⋯ ⋯))) t

If γ₁ and γ₂ are two paths, then γ₁.trans γ₂ --> [1/(2n + 4), 1] --> [0, (2n + 2)/(2n + 3)] (so taking [1/(2n + 4), (2n + 3)/(2n + 4)]) is the same as γ₁ --> [1/(n+2), 1], added to γ₂ --> [0, (n+1)/(n+2)]

theorem SplitProperties.trans_second_part_second_part {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) (n : ℕ) (t : ↑unitInterval) : (SplitDipath.SecondPart (SplitDipath.SecondPart (γ₁.trans γ₂) (Fraction.ofPos ⋯)) (Fraction ⋯ ⋯)) t = (SplitDipath.SecondPart γ₂ (Fraction ⋯ ⋯)) t

If γ₁ and γ₂ are two paths, then γ₁.trans γ₂ --> [1/(2n + 4), 1] --> [(2n+2)/(2n+3), 1] (so to [(2n+3)/(2n+4), 1]) is the same as γ₂ --> [(n+1)/(n+2), 1]

theorem SplitProperties.trans_image_inv_eq_first {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) (n : ℕ) : (γ₁.trans γ₂) (Fraction.ofPos ⋯) = γ₁ (Fraction.ofPos ⋯)

If γ₁ and γ₂ are two paths, then γ₁.trans γ₂ evaluated at 1/(2n+2) is the same as γ₁ evaluated at 1/(n+1).

theorem SplitProperties.second_part_trans_eval_at_end {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ : X} (γ₁ : Dipath x₀ x₁) (γ₂ : Dipath x₁ x₂) (n : ℕ) : (SplitDipath.SecondPart (γ₁.trans γ₂) (Fraction.ofPos ⋯)) (Fraction ⋯ ⋯) = γ₂ (Fraction ⋯ ⋯)

If γ₁ and γ₂ are two paths, then γ₁.trans γ₂ --> [1/(2n+4), 1] evaluated at (2n+2)/(2n+3) is the same as γ₂ evaluated at (n+1)/(n+2).