𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ liftIco p a f ↑x = f x
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIco p a f ↑x = f x
have : (equivIco p a) x = ⟨x, hx⟩ := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]
  rfl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ restrict (Ico a (a + p)) f { val := x, property := hx } = f x
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ liftIco p a f ↑x = f x
rw [liftIco, comp_apply, this]
no goals
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
this : ↑(equivIco p a) ↑x = { val := x, property := hx }
⊢ restrict (Ico a (a + p)) f { val := x, property := hx } = f x
rfl
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = ↑(equivIco p a).symm { val := x, property := hx }
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑(equivIco p a) ↑x = { val := x, property := hx }
rw [Equiv.apply_eq_iff_eq_symm_apply]
no goals
𝕜 : Type u_1
B : Type u_2
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = ↑(equivIco p a).symm { val := x, property := hx }
rfl