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

Goal state before:
pp: β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ x1 ∩ x2) B₁ B₂)

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ closure[inst✝] (range f) ⊆ C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).domRestrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.domRestrict topologicalSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis (image2 (fun x1 x2 ↦ f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
y : β
⊢ y ∈ sβ → f a y = g y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ ContinuousOn (fun b ↦ (a, b)) sβ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun b ↦ (a, b)
⊢ MapsTo (fun b ↦ (a, b)) sβ (sα ×ˢ sβ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
⊢ ContinuousOn (f a) sβ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : DecidableEq ι
l : Filter Y
f : Y → (i : ι) → A i
x : (i : ι) → A i
hf : Tendsto f l (𝓝 x)
i : ι
g : Y → A i
xi : A i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 ↦ Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
y : α
⊢ y ∈ sα → f y b = g y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ ContinuousOn (fun a ↦ (a, b)) sα

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i ↦ Fin.cons (f i) (g i) 0) l (𝓝 (Fin.cons x y 0))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun a ↦ (a, b)
⊢ MapsTo (fun a ↦ (a, b)) sα (sα ×ˢ sβ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β → γ
sα : Set α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
⊢ ContinuousOn (fun a ↦ f a b) sα

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → A 0
g : Y → (j : Fin n) → A j.succ
l : Filter Y
x : A 0
y : (j : Fin n) → A j.succ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.cons (f i_1) (g i_1) i.succ) l (𝓝 (Fin.cons x y i.succ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i ↦ Fin.snoc (f i) (g i) (Fin.last n)) l (𝓝 (Fin.snoc x y (Fin.last n)))

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst✝] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst✝] (range f) ⊆ C
⊢ Disjoint C (range g)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.snoc (f i_1) (g i_1) i.castSucc) l (𝓝 (Fin.snoc x y i.castSucc))

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
h : IsInducing (Sum.elim f g)
⊢ Disjoint (closure[inst✝] (range f)) (range g)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ IsTopologicalBasis (⋃ i, image Subtype.val '' b i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i_1 ↦ i.insertNth (f i_1) (g i_1) i) l (𝓝 (i.insertNth x y i))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, inst✝] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
i : Fin (n + 1)
f : Y → A i
g : Y → (j : Fin n) → A (i.succAbove j)
l : Filter Y
x : A i
y : (j : Fin n) → A (i.succAbove j)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n), Tendsto (fun i_1 ↦ i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst✝] (⋃ i, g i)
v : ι → Set α
hv : ∀ (i : ι), IsOpen[t] (v i)
he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s
⊢ (f ⁻¹' ⋃ i, g i) ∩ s = (⋃ i, v i) ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
s : Set α
hf : IsInducing f
⊢ ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s

Tactic:
simp [ContinuousOn, ContinuousWithinAt, ← hf.map_nhdsWithin_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ u, IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
s : Set α
hf : IsInducing f
⊢ ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis ∅
⊢ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ ∅, ∀ t₂ ∈ ∅, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ∅, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ ∅ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis {∅}
⊢ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ {∅}, ∀ t₂ ∈ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ {∅} = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst✝¹] s
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
⊢ SeparableSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
⊢ SeparableSpace (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ k, ⋃ (_ : k < n + 1), s k

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ⋃ x, accumulate s x = ⋃ x, s x

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : α → Set β
⊢ accumulate s ⊥ = s ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
⊢ accumulate s 0 = s 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
⊢ Disjoint (accumulate s i) (s j)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
⊢ ⇑(partialSups f) = accumulate f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
⊢ ContinuousOn f (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s (n + 1) ⊆ s k

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
⊢ ContinuousOn f (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n : ℕ
⊢ ∃ m, accumulate s n ⊆ s m

Tactic:
by

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) ↔ ∃ n, s n = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ comk (fun x ↦ x ∈ B) empty_mem subset_mem union_mem ≤ cofinite

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
⊢ IsBounded sᶜ ↔ IsCobounded s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
⊢ IsBounded ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
x : α
⊢ IsBounded {x}

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
⊢ IsBounded s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s t : Set α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Bornology α
inst✝ : Finite ι
s : ι → Set α
⊢ IsBounded (⋃ i, s i) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u : Set β
h : u ∈ 𝓝ˢ t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s] (s ∩ f ⁻¹' t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous[inst✝¹, inst✝] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)

Tactic:
by

Goal state after: