α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
rw [isOpen_iff_ball_subset]
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s

case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s) ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
constructor <;> intro h x hx
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
case mp
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
obtain ⟨V, hV, hV'⟩ := h x hx
no goals
case mp.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
exact
  ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
    (ball_mono interior_subset x).trans hV'⟩
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
case mpr
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
obtain ⟨V, hV, -, hV'⟩ := h x hx
no goals
case mpr.intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.91712
inst✝ : UniformSpace α
s : Set α
h : ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
exact ⟨V, hV, hV'⟩