α : Type u
β : Type v
γ : Type ?u.158230
δ : Type ?u.158233
ε : Type ?u.158236
ζ : Type ?u.158239
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
t : Set ↑s
⊢ (∀ (x : α) (h : x ∈ s), ↑{ val := x, property := h } ∈ closure (val '' t)) ↔ s ⊆ closure (val '' t)
α : Type u
β : Type v
γ : Type ?u.158230
δ : Type ?u.158233
ε : Type ?u.158236
ζ : Type ?u.158239
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
t : Set ↑s
⊢ Dense t ↔ s ⊆ closure (val '' t)
rw [inducing_subtype_val.dense_iff, SetCoe.forall]
no goals
α : Type u
β : Type v
γ : Type ?u.158230
δ : Type ?u.158233
ε : Type ?u.158236
ζ : Type ?u.158239
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
t : Set ↑s
⊢ (∀ (x : α) (h : x ∈ s), ↑{ val := x, property := h } ∈ closure (val '' t)) ↔ s ⊆ closure (val '' t)
rfl