case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type ?u.15155
γ : Type ?u.15158
ι : Type ?u.15161
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ ∃ x, IsGδ x✝ ∧ Dense x✝
α : Type u_1
β : Type ?u.15155
γ : Type ?u.15158
ι : Type ?u.15161
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
⊢ (∀ᶠ (x : α) in residual α, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ (x : α), x ∈ t → p x
convert@mem_residual _ _ _ p
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type ?u.15155
γ : Type ?u.15158
ι : Type ?u.15161
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ IsGδ x✝ ∧ Dense x✝ ∧ x✝ ⊆ p
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type ?u.15155
γ : Type ?u.15158
ι : Type ?u.15161
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ ∃ x, IsGδ x✝ ∧ Dense x✝
simp_rw [exists_prop, @and_comm ((_ : Set α) ⊆ p), and_assoc]
no goals
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type ?u.15155
γ : Type ?u.15158
ι : Type ?u.15161
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ IsGδ x✝ ∧ Dense x✝ ∧ x✝ ⊆ p
rfl