mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsCoinducing (g ∘ f)
⊢ inst✝ ≤ coinduced g inst✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : Y ≃ₜ Z
f : X → Y
h : IsOpenQuotientMap (⇑e ∘ f)
⊢ IsOpenQuotientMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ map (⇑h.symm) (𝓝 (h x)) = 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsCoinducing f
hf' : Injective f
⊢ IsOpenMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
⊢ tβ = induced f tα ↔ ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X → Prop
q : Y → Prop
f : X ≃ₜ Y
hs : IsClopen {x | p x}
ht : IsClopen {y | q y}
⊢ IsClosed[inst✝¹] {x | p x ↔ q (f x)}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
inst✝ : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ Continuous[nhdsAdjoint a l, inst✝] f ↔ Tendsto f l (𝓝 (f a))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ coinduced f (nhdsAdjoint a l) ≤ x✝ ↔ nhdsAdjoint (f a) (map f l) ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst✝²] (⇑e ⁻¹' s) ↔ IsOpen[inst✝¹] s
s : Set X
⊢ IsOpen[inst✝²] s → IsOpen[inst✝¹] (e.invFun ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsClosed[induced f t] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure[induced f t] s ↔ f a ∈ closure[t] (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen[inst✝²] (⇑e ⁻¹' s) ↔ IsOpen[inst✝¹] s
s : Set X
⊢ IsOpen[inst✝¹] (⇑e.symm ⁻¹' s) ↔ IsOpen[inst✝²] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed[induced f t] s ↔ ∀ (a : α), f a ∈ closure[t] (f '' s) → a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: ⊢ ⨅ s ∈ {s | False ∈ s ∧ s ∈ {{True}}}, 𝓟 s = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ IsQuotientMap (g ∘ f) ↔ IsQuotientMap g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ≃ Y
hf : IsInducing ⇑f
⊢ Continuous[inst✝¹, inst✝¹] (⇑f ∘ f.invFun)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
q : Prop
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
e : X ≃ Y
⊢ ∀ (s : Set Y), IsOpen[inst✝⁴] (⇑e ⁻¹' s) ↔ IsOpen[inst✝³] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ Continuous[inst✝, _] p ↔ IsOpen[inst✝] {x | p x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ IsClosed[⨆ i, t i] s ↔ ∀ (i : ι), IsClosed[t i] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' interior (f ∘ e ⁻¹' s) = f '' interior (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : IsQuotientMap f
⊢ Continuous[inst✝¹, inst✝] g ↔ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' frontier (f ∘ e ⁻¹' s) = f '' frontier (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' closure[inst✝¹] (f ∘ e ⁻¹' s) = f '' closure[inst✝] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝] (id '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝] (g ∘ f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
f_surj : Surjective f
h : IsOpenMap (g ∘ f)
s : Set Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (g '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
⊢ IsOpen[inst✝] (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hf' : Continuous[inst✝¹, inst✝] f
s : Set X
⊢ map f (𝓝ˢ s) = 𝓝ˢ (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
open_map : IsOpenMap f
cont : Continuous[inst✝¹, inst✝] f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst✝] s ⊆ closure[inst✝¹] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : IsOpenMap f
h₂ : Injective f
h₃ : Continuous[inst✝¹, inst✝] f
s : Set X
hs' : IsClosed[inst✝¹] s
⊢ f ⁻¹' closure[inst✝] (f '' s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
hfc : Continuous[inst✝¹, inst✝] f
s : Set Y
⊢ f ⁻¹' frontier s = frontier (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ ClusterPt x (comap f l)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ≤ 𝓟 {x}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : AccPt (f x) l
⊢ AccPt x (comap f l)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpenMap f ↔ ∀ {u : Set X}, IsClosed[inst✝¹] u → IsClosed[inst✝] (kernImage f u)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ comap f (𝓟 (f '' s)ᶜ) ≤ 𝓟 sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpenMap f ↔ ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
u : Set X
hu : IsOpen[inst✝¹] u
⊢ f '' u ⊆ interior (f '' u)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.WithTopology

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
s : Set (WithTopology X t)
⊢ IsClosed s ↔ IsClosed[t] (toTopology t ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst✝] (kernImage f s) ⊆ kernImage f (closure[inst✝¹] s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ IsClosed[inst✝] (id '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
⊢ IsClosedMap g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f' : Y → X
h : Continuous[inst✝, inst✝¹] f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝] (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed[inst✝¹] s → s.Nonempty → IsClosed[inst✝] (f '' s)
⊢ IsClosedMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {u : Set X}, IsOpen[inst✝¹] u → IsOpen[inst✝] (kernImage f u)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed[inst✝] (range f)
⊢ IsClosedMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), closure[inst✝] (f '' s) ⊆ f '' closure[inst✝¹] s
c : Set X
hc : IsClosed[inst✝¹] c
⊢ f '' closure[inst✝¹] c = f '' c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {y : Y}, comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in 𝓝 x₀, p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∃ᶠ (y : Y) in 𝓝 y₀, ∃ x ∈ f ⁻¹' {y}, p x
⊢ ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in 𝓝 x₀, p x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
F : Filter X
⊢ (map f F).lift' closure[inst✝] = map f (F.lift' closure[inst✝¹])

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
⊢ Continuous[inst✝, instTopologicalSpaceProd] fun y ↦ (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
⊢ Continuous[inst✝¹, instTopologicalSpaceProd] fun x ↦ (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Z : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
α : Type u_5
f : X → α → Z
s : Set α
t : Set Z
ht : IsClosed[inst✝] t
hf : ∀ a ∈ s, Continuous[inst✝¹, inst✝] fun x ↦ f x a
⊢ IsClosed[inst✝¹] {x | MapsTo (f x) s t}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ MapClusterPt y F f ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen[inst✝] (f '' s)
⊢ IsOpen[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
⊢ Sort ?u.38

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ IsOpenEmbedding f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc1] fun p ↦ f p.1 p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
hg : IsOpenEmbedding g
⊢ IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
W : Type u_1
Z✝ : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.29
Y : Type ?u.32
Z : Type ?u.38
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
⊢ Sort ?u.55

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ AccPt x (comap f l) ↔ AccPt (f x) l

Tactic:
by

Goal state after: