[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hg : Inducing g
hf : Inducing f
⊢ inst✝³ = TopologicalSpace.induced (g ∘ f) inst✝¹
[PROOFSTEP]
rw [hf.induced, hg.induced, induced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ inst✝³ ≤ induced f inst✝²
[PROOFSTEP]
rwa [← continuous_iff_le_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝³
[PROOFSTEP]
rw [hgf.induced, ← induced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝¹)
[PROOFSTEP]
exact induced_mono hg.le_induced
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))
[PROOFSTEP]
simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ MapClusterPt (f a) l f ↔ ClusterPt a l
[PROOFSTEP]
delta MapClusterPt ClusterPt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ NeBot (𝓝 (f a) ⊓ map f l) ↔ NeBot (𝓝 a ⊓ l)
[PROOFSTEP]
rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
ι : Type u_5
f : ι → β
g : β → γ
a : Filter ι
b : β
hg : Inducing g
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (g ∘ f) a (𝓝 (g b))
[PROOFSTEP]
rw [hg.nhds_eq_comap, tendsto_comap_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
⊢ Continuous f ↔ Continuous (g ∘ f)
[PROOFSTEP]
simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Inducing f
x : α
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
[PROOFSTEP]
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
⊢ Inducing f ↔ Inducing (g ∘ f)
[PROOFSTEP]
refine' ⟨fun h => hg.comp h, fun hgf => inducing_of_inducing_compose _ hg.continuous hgf⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous f
[PROOFSTEP]
rw [hg.continuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous (g ∘ f)
[PROOFSTEP]
exact hgf.continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ closure s = f ⁻¹' closure (f '' s)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
x : α
⊢ x ∈ closure s ↔ x ∈ f ⁻¹' closure (f '' s)
[PROOFSTEP]
rw [Set.mem_preimage, ← closure_induced, hf.induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s
[PROOFSTEP]
rw [hf.induced, isClosed_induced_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsClosed s ↔ ∀ (x : α), f x ∈ closure (f '' s) → x ∈ s
[PROOFSTEP]
rw [hf.induced, isClosed_induced_iff']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
[PROOFSTEP]
rw [hf.induced, isOpen_induced_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ Dense s ↔ ∀ (x : α), f x ∈ closure (f '' s)
[PROOFSTEP]
simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : _root_.Embedding (g ∘ f)
a₁ a₂ : α
h : f a₁ = f a₂
⊢ (g ∘ f) a₁ = (g ∘ f) a₂
[PROOFSTEP]
simp [h, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DiscreteTopology Y
f : X → Y
hf : _root_.Embedding f
x : X
⊢ 𝓝 x = pure x
[PROOFSTEP]
rw [hf.nhds_eq_comap, nhds_discrete, comap_pure, ← image_singleton, hf.inj.preimage_image, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ (∀ (x : Set β), IsOpen xᶜ ↔ IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set β), IsClosed s ↔ IsClosed (f ⁻¹' s)
[PROOFSTEP]
simp only [isOpen_compl_iff, preimage_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hg : QuotientMap g
hf : QuotientMap f
⊢ inst✝¹ = coinduced (g ∘ f) inst✝³
[PROOFSTEP]
rw [hg.right, hf.right, coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ inst✝¹ ≤ coinduced g inst✝²
[PROOFSTEP]
rw [hgf.right, ← coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝³) ≤ coinduced g inst✝²
[PROOFSTEP]
exact coinduced_mono hf.coinduced_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : QuotientMap f
⊢ Continuous g ↔ Continuous (g ∘ f)
[PROOFSTEP]
rw [continuous_iff_coinduced_le, continuous_iff_coinduced_le, hf.right, coinduced_compose]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
hs : IsOpen s
⊢ IsOpen (id '' s)
[PROOFSTEP]
rwa [image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g ∘ f '' s)
[PROOFSTEP]
rw [image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ : α → β
g : β → γ
f : α → β
hg : IsOpenMap g
hf : IsOpenMap f
s : Set α
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))
[PROOFSTEP]
exact hg _ (hf _ hs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
⊢ IsOpen (f '' univ)
[PROOFSTEP]
exact hf _ isOpen_univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))
[PROOFSTEP]
rw [map_map, hgf.comp_eq_id, map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f✝ f : α → β
h : ∀ (x : α), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f
x : α
g : β → α
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : Function.RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)
[PROOFSTEP]
rw [hgx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
[PROOFSTEP]
rw [← compl_subset_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ (closure (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure s)ᶜ
[PROOFSTEP]
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
s : Set β
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
[PROOFSTEP]
simpa only [frontier_eq_closure_inter_closure, preimage_inter] using
  inter_subset_inter hf.preimage_closure_subset_closure_preimage hf.preimage_closure_subset_closure_preimage
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : IsOpenMap f
hfc : Continuous f
s : Set β
⊢ f ⁻¹' frontier s = frontier (f ⁻¹' s)
[PROOFSTEP]
simp only [frontier_eq_closure_inter_closure, preimage_inter, preimage_compl,
  hf.preimage_closure_eq_closure_preimage hfc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), f '' interior s ⊆ interior (f '' s)
u : Set α
hu : IsOpen u
⊢ f '' u = f '' interior u
[PROOFSTEP]
rw [hu.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsClosed s
⊢ IsClosed (id '' s)
[PROOFSTEP]
rwa [image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
s : Set α
hs : IsClosed s
⊢ IsClosed (g ∘ f '' s)
[PROOFSTEP]
rw [image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : IsClosedMap g
hf : IsClosedMap f
s : Set α
hs : IsClosed s
⊢ IsClosed (g '' (f '' s))
[PROOFSTEP]
exact hg _ (hf _ hs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
rw [image_eq_preimage_of_inverse r_inv l_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)
[PROOFSTEP]
exact hs.preimage h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
⊢ IsClosedMap f
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
cases' eq_empty_or_nonempty s with h2s h2s
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)
[PROOFSTEP]
simp_rw [h2s, image_empty, isClosed_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : Set.Nonempty s
⊢ IsClosed (f '' s)
[PROOFSTEP]
exact h s hs h2s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
⊢ IsClosedMap f
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
[PROOFSTEP]
rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))
[PROOFSTEP]
rw [image_preimage_eq_inter_range]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)
[PROOFSTEP]
exact ht.inter h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), closure (f '' s) ⊆ f '' closure s
c : Set α
hc : IsClosed c
⊢ f '' closure c = f '' c
[PROOFSTEP]
rw [hc.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ IsClosedMap f ↔ ∀ (s : Set α) (y : β), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
[PROOFSTEP]
simp [MapClusterPt, isClosedMap_iff_closure_image, subset_def, mem_closure_iff_clusterPt, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ Filter.lift' (map f F) closure = map f (Filter.lift' F closure)
[PROOFSTEP]
rw [map_lift'_eq2 (monotone_closure β), map_lift'_eq (monotone_closure α)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ Filter.lift' F (closure ∘ image f) = Filter.lift' F (image f ∘ closure)
[PROOFSTEP]
congr
[GOAL]
case e_h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
⊢ closure ∘ image f = image f ∘ closure
[PROOFSTEP]
ext s : 1
[GOAL]
case e_h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter α
s : Set α
⊢ (closure ∘ image f) s = (image f ∘ closure) s
[PROOFSTEP]
exact f_closed.closure_image_eq_of_continuous f_cont s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
F : Filter α
f : α → β
f_closed : IsClosedMap f
f_cont : Continuous f
y : β
⊢ MapClusterPt y F f ↔ NeBot (Filter.lift' F closure ⊓ 𝓟 (f ⁻¹' {y}))
[PROOFSTEP]
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont, ← comap_principal, ←
  map_neBot_iff f, Filter.push_pull, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set α
h : IsOpen (f '' s)
⊢ IsOpen s
[PROOFSTEP]
convert ← h.preimage hf.toEmbedding.continuous
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set α
h : IsOpen (f '' s)
⊢ f ⁻¹' (f '' s) = s
[PROOFSTEP]
apply preimage_image_eq _ hf.inj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ Tendsto (g ∘ f) (𝓝 a) l ↔ Tendsto g (𝓝 (f a)) l
[PROOFSTEP]
rw [Tendsto, ← map_map, hf.map_nhds_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ map g (𝓝 (f a)) ≤ l ↔ Tendsto g (𝓝 (f a)) l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsOpen s ↔ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [hf.open_iff_image_open, image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ OpenEmbedding f
[PROOFSTEP]
simp only [openEmbedding_iff_embedding_open, embedding_iff, inducing_iff_nhds, *, and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
[PROOFSTEP]
exact fun a => le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 a) _ h₂ ▸ comap_mono (h₃.nhds_le _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
hg : OpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)
[PROOFSTEP]
simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, Filter.map_le_map_iff hg.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : OpenEmbedding g
⊢ OpenEmbedding (g ∘ f) ↔ OpenEmbedding f
[PROOFSTEP]
simp only [openEmbedding_iff_continuous_injective_open, ← hg.isOpenMap_iff, ← hg.1.continuous_iff, hg.inj.of_comp_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed s
[PROOFSTEP]
rw [← preimage_image_eq s hf.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))
[PROOFSTEP]
exact h.preimage hf.continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set β
hs : s ⊆ range f
⊢ IsClosed s ↔ IsClosed (f ⁻¹' s)
[PROOFSTEP]
rw [hf.closed_iff_image_closed, image_preimage_eq_of_subset hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ ClosedEmbedding f
[PROOFSTEP]
refine closedEmbedding_of_embedding_closed ⟨⟨?_⟩, h₂⟩ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝² = induced f inst✝¹
[PROOFSTEP]
refine h₁.le_induced.antisymm fun s hs => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
[PROOFSTEP]
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]
