case mp
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
⊢ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)

case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
⊢ Dense s
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ Dense s ↔ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
constructor <;> intro h
case mp.intro
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
U : Set α
U_op : IsOpen U
x : α
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
case mp
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
⊢ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
rintro U U_op ⟨x, x_in⟩
no goals
case mp.intro
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
U : Set α
U_op : IsOpen U
x : α
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
exact mem_closure_iff.1 (h _) U U_op x_in
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ x ∈ closure s
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
⊢ Dense s
intro x
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ ∀ (o : Set α), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ x ∈ closure s
rw [mem_closure_iff]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
U : Set α
U_op : IsOpen U
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ ∀ (o : Set α), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
intro U U_op x_in
no goals
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
U : Set α
U_op : IsOpen U
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
exact h U U_op ⟨_, x_in⟩