no goals
𝕜 : Type ?u.182740
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.182746
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.182841
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.182931
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a b : ℝ
hab : a < b
⊢ Set.Nonempty (interior (Ioc a b))
simp only [interior_Ioc, nonempty_Ioo, hab]
no goals
𝕜 : Type ?u.182740
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.182746
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.182841
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.182931
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ioc a b)
simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]