R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) '' s)
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
⊢ IsOpenMap ↑(mk N)
intro s s_op
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) ⁻¹' (↑(mk N) '' s))
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) '' s)
change IsOpen (mk N ⁻¹' (mk N '' s))
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => ↑x + y) '' s)
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (↑(mk N) ⁻¹' (↑(mk N) '' s))
rw [quotient_ring_saturate]
no goals
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
N : Ideal R
inst✝ : TopologicalRing R
s : Set R
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => ↑x + y) '' s)
exact isOpen_iUnion fun ⟨n, _⟩ => isOpenMap_add_left n s s_op