R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) ↔ DiscreteTopology A
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ IsAdic ⊥ ↔ DiscreteTopology A
rw [isAdic_iff]
case mp
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A

case mpr
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) ↔ DiscreteTopology A
constructor
case mp.intro
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ DiscreteTopology A
case mp
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A
rintro ⟨h, _h'⟩
case mp.intro
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen {0}
case mp.intro
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ DiscreteTopology A
rw [discreteTopology_iff_open_singleton_zero]
no goals
case mp.intro
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen {0}
simpa using h 1
case mpr
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
case mpr
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
intros
case mpr.left
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)

case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
case mpr
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
constructor
no goals
case mpr.left
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
simp
case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ∃ n, ↑(⊥ ^ n) ⊆ U
case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
intro U U_nhds
case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ↑(⊥ ^ 1) ⊆ U
case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ∃ n, ↑(⊥ ^ n) ⊆ U
use 1
no goals
case mpr.right
R : Type ?u.334870
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_1
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ↑(⊥ ^ 1) ⊆ U
simp [mem_of_mem_nhds U_nhds]