no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : Homotopy p₀ q₀
G : Homotopy p₁ q₁
t : ↑I
⊢ 0 ≤ 1 / 2
norm_num
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : Homotopy p₀ q₀
G : Homotopy p₁ q₁
t : ↑I
⊢ 1 / 2 ≤ 1
norm_num
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : Homotopy p₀ q₀
G : Homotopy p₁ q₁
t : ↑I
⊢ (if ↑(t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }).snd ≤ 1 / 2 then
      extend (eval F (t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }).fst)
        (2 * ↑(t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }).snd)
    else
      extend (eval G (t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }).fst)
        (2 * ↑(t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }).snd - 1)) =
    x₁
norm_num