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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : {u | GenerateOpen s u} = s
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] = IsOpen[generateFrom s]

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
u : ℕ → Set X
u_cov : s ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t
v : ℕ → Set X
v_cov : t ⊆ ⋃ n, v n
v_props : ∀ (n : ℕ), IsOpen[inst✝] (v n) ∧ Disjoint (closure[inst✝] (v n)) s
open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst✝] (u₀ n)) → IsOpen[inst✝] (⋃ n, u₀ n \ closure[inst✝] (a n))
cover_lemma :
  ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
    h₀ ⊆ ⋃ n, u₀ n →
      (∀ (n : ℕ), Disjoint (closure[inst✝] (v₀ n)) h₀) → h₀ ⊆ ⋃ n, u₀ n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v₀ m)
x : X
n : ℕ
xinun : x ∈ (fun n ↦ u n \ closure[inst✝] (⋃ m, ⋃ (_ : m ≤ n), v m)) n
m : ℕ
xinvm : x ∈ v m
⊢ n ≤ m

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ inst✝¹ = induced (g ∘ f) inst✝

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ IsInducing (g ∘ f) ↔ IsInducing 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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝¹, inst✝²] f
hg : Continuous[inst✝², inst✝] g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝¹

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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Set α
⊢ IsOpen[t₂] U ↔ U = ∅ ∨ U = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
C : Set α
⊢ IsClosed[t₂] C ↔ C = ∅ ∨ C = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
s : Set α
h : s.Nonempty
⊢ Dense s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : IndiscreteTopology β
f : α → β
⊢ ∀ (s : Set β), IsOpen[inst✝¹] s → IsOpen[t₂] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
s : Set α
⊢ Dense s ↔ s = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ DenseRange f ↔ Surjective f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (f ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Goal state after:
β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (⋃ i ∈ s, f ⁻¹' {i})
Module: Mathlib.Topology.Order

Goal state before:
pp: β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure[inst✝] ((fun x ↦ ∅) x✝)) s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure[inst✝] ((fun x ↦ univ) x✝)) ∅

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → IsOpen[t₁] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t u : Set X
⊢ SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) 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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ MapClusterPt (f x) l f ↔ ClusterPt x l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen[t] xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
by

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

Goal state before:
pp: Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced 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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ Continuous[inst✝¹, inst✝²] f ↔ Continuous[inst✝¹, inst✝] (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_4
β : Type u_5
e : α ≃ β
⊢ TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : NontrivialTopology α
⊢ Nontrivial α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
⊢ WithTopology.instTopologicalSpace α ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst✝] (s ∪ t)
⊢ IsOpen[inst✝] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom 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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ closure[inst✝] s = f ⁻¹' closure[inst✝¹] (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert ∅ s) = generateFrom 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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst✝] s ↔ ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t ↦ 𝓝 a) t

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
⊢ h.trans h.symm = Homeomorph.refl 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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsClosed[inst✝] s
⊢ ∃ c, IsClosed[inst✝¹] c ∧ f '' s = c ∩ range 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
⊢ h.symm.trans h = Homeomorph.refl 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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s) → x ∈ 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
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.LeftInverse g ⇑f

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
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Function.RightInverse g ⇑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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[inst✝] s ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
⊢ 𝓝 a = pure a ⊔ f

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
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Continuous[inst✝⁴, inst✝⁵] g

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
⊢ range ⇑h = univ

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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
hs : IsOpen[inst✝] s
⊢ ∃ c, IsOpen[inst✝¹] c ∧ f '' s = c ∩ range 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
⊢ IsInducing (⇑h.symm ∘ ⇑h)

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 Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ Dense s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s)

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
⊢ IsQuotientMap (⇑h ∘ ⇑h.symm)

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
s : Set X
⊢ IsOpen[inst✝] (⇑h '' s) ↔ IsOpen[inst✝¹] s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : IndiscreteTopology Y
f : X → Y
hf : IsInducing f
⊢ inst✝¹ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsClosed[inst✝] (s ∪ t)
⊢ IsClosed[inst✝] s

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
s : Set Y
⊢ IsClosed[inst✝¹] (⇑h ⁻¹' s) ↔ IsClosed[inst✝] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen[t] {b}

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : NontrivialTopology X
f : X → Y
hf : IsInducing f
⊢ ¬NontrivialTopology Y → ¬NontrivialTopology X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
a : α
⊢ 𝓝 a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : IndiscreteTopology α
x : α
f : Filter α
inst✝ : f.NeBot
⊢ ClusterPt x 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
s : Set X
⊢ IsClosed[inst✝] (⇑h '' s) ↔ IsClosed[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology α ↔ ∃ x y, ¬Inseparable x y

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 : IsEmbedding g
⊢ IsEmbedding (g ∘ f) ↔ IsEmbedding f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ t = ⊤ ↔ ∀ (x y : α), Inseparable x 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
⊢ (∀ (x : Set Y), IsOpen[inst✝¹] (f ⁻¹' xᶜ) ↔ IsOpen[inst✝] xᶜ) ↔
    ∀ (s : Set Y), IsClosed[inst✝¹] (f ⁻¹' s) ↔ IsClosed[inst✝] s

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
s : Set X
⊢ ⇑h '' closure[inst✝¹] s = closure[inst✝] (⇑h '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ t ≠ ⊤ ↔ ∃ x y, ¬Inseparable x 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 : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsOpen[inst✝¹] (f ⁻¹' s)

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
s : Set X
⊢ ⇑h '' interior s = interior (⇑h '' 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 : IsCoinducing g
hf : IsCoinducing f
⊢ inst✝ = coinduced (g ∘ f) inst✝²

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
s : Set X
⊢ ⇑h '' frontier s = frontier (⇑h '' s)

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
h : X ≃ₜ Y
f : Y → Z
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst✝¹] (g ⁻¹' s) ↔ IsOpen[inst✝] s

Tactic:
← hgf.isOpen_preimage,

Goal state after:
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 : IsCoinducing f
hgf : IsCoinducing (g ∘ f)
s : Set Z
⊢ IsOpen[inst✝¹] (g ⁻¹' s) ↔ IsOpen[inst✝²] (g ∘ f ⁻¹' s)
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f : α → β
g : γ → α
t₂ : TopologicalSpace β
t₁ : TopologicalSpace γ
⊢ Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f : α → β
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
⊢ Continuous[t₂, t₃] 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 : IsCoinducing f
⊢ IsCoinducing (g ∘ f) ↔ IsCoinducing g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous[t₁, t₂] f
⊢ Continuous[t₁, t₃] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f

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
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
T : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
⊢ Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[_, t₂] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous[iSup t₁, t₂] f ↔ ∀ (i : ι), Continuous[t₁ i, t₂] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, _] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous[t₁, iInf t₂] f ↔ ∀ (i : ι), Continuous[t₁, t₂ i] f

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
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

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 : X ≃ₜ Y
f : Y → Z
h : IsOpenQuotientMap (f ∘ ⇑e)
⊢ IsOpenQuotientMap f

Tactic:
by

Goal state after: