no goals
𝕜 : Type ?u.181211
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.181217
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.181312
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.181402
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a b : ℝ
hab : a < b
⊢ Set.Nonempty (interior (Ico a b))
simp only [interior_Ico, nonempty_Ioo, hab]
no goals
𝕜 : Type ?u.181211
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.181217
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.181312
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.181402
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ico a b)
simp only [Ico_eq_empty hab, uniqueDiffOn_empty]