α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ s ∈ 𝓝 a ↔ ∃ u, u ∈ 𝓝 (f a) ∧ f ⁻¹' u ⊆ s
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ ∃ u, u ∈ 𝓝 (f a) ∧ f ⁻¹' u ⊆ s
letI := T.induced f
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ s ∈ 𝓝 a ↔ ∃ u, u ∈ 𝓝 (f a) ∧ f ⁻¹' u ⊆ s
simp only [mem_nhds_iff, isOpen_induced_iff, exists_prop, Set.mem_setOf_eq]
case mp
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) → ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

case mpr
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
constructor
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
v : Set α
openv : IsOpen v
usub : f ⁻¹' v ⊆ s
au : a ∈ f ⁻¹' v
⊢ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
case mp
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) → ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
no goals
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
v : Set α
openv : IsOpen v
usub : f ⁻¹' v ⊆ s
au : a ∈ f ⁻¹' v
⊢ ∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
case mpr.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen v
amem : f a ∈ v
⊢ ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
case mpr
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ u, (∃ t, t ⊆ u ∧ IsOpen t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) → ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
no goals
case mpr.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.43330
f✝ : α → β
ι : Sort ?u.43337
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen v
amem : f a ∈ v
⊢ ∃ t, t ⊆ s ∧ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩