α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ idRel ⊆ ⋂₀ (𝓤 α).sets
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ idRel ⊆ 𝓢 α
unfold separationRel
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ (a : α), (a, a) ∈ ⋂₀ (𝓤 α).sets
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ idRel ⊆ ⋂₀ (𝓤 α).sets
rw [idRel_subset]
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ (x, x) ∈ ⋂₀ (𝓤 α).sets
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
⊢ ∀ (a : α), (a, a) ∈ ⋂₀ (𝓤 α).sets
intro x
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ ∀ (t : Set (α × α)), t ∈ 𝓤 α → (x, x) ∈ t
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ (x, x) ∈ ⋂₀ (𝓤 α).sets
suffices ∀ t ∈ 𝓤 α, (x, x) ∈ t by simpa only [refl_mem_uniformity]
no goals
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
⊢ ∀ (t : Set (α × α)), t ∈ 𝓤 α → (x, x) ∈ t
exact fun t => refl_mem_uniformity
no goals
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u_1
inst✝ : UniformSpace α
x : α
this : ∀ (t : Set (α × α)), t ∈ 𝓤 α → (x, x) ∈ t
⊢ (x, x) ∈ ⋂₀ (𝓤 α).sets
simpa only [refl_mem_uniformity]