𝕜 : Type u_1
B : Type ?u.15815
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))
𝕜 : Type u_1
B : Type ?u.15815
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen {x | (fun x => toIcoMod hp a x = toIocMod hp a x) x}
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
no goals
𝕜 : Type u_1
B : Type ?u.15815
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen (⋃ (z : ℤ), Ioo (a + z • p) (a + p + z • p))
exact isOpen_iUnion fun i => isOpen_Ioo