Theorem: MvPowerSeries.topology_eq_ideals_basis_topology (DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ := MvPowerSeries.WithPiTopology.topologicalSpace σ α
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ' := (toRingSubgroupsBasis σ α).topology
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
erw [TopologicalAddGroup.ext_iff_nhds_zero τ τ']
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0
Tactic:
ext s
State after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0

State before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Tactic:
rw [(RingSubgroupsBasis.hasBasis_nhds (toRingSubgroupsBasis σ α) 0).mem_iff]
State after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Tactic:
simp only [sub_zero, Submodule.mem_toAddSubgroup, exists_true_left, true_and]
State after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
refine' ⟨_, fun ⟨d, hd⟩ => (@nhds _ τ 0).sets_of_superset (basis_mem_nhds_zero σ α d) hd⟩
State after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
rw [nhds_pi, Filter.mem_pi]
State after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ s) → ∃ i, {b | b ∈ basis σ α i} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ s) → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
rintro ⟨D, hD, t, ht, ht'⟩
State after:
case a.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ s

State before:
case a.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
use Finset.sup hD.toFinset id
State after:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ s

State before:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ s
Tactic:
apply subset_trans _ ht'
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ D.pi t

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ D.pi t
Tactic:
intro f hf e he
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ f e ∈ t e

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ f e ∈ t e
Tactic:
rw [← coeff_eq_apply f e, hf e]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ 0 ∈ t e

σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ 0 ∈ t e

σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id
Tactic:
exact mem_of_mem_nhds (ht e)
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id
Tactic:
. have he' : e ∈ (Finite.toFinset hD) := by
    simp only [id_eq, Finite.mem_toFinset]
    exact he
  apply Finset.le_sup he'
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id
Tactic:
have he' : e ∈ (Finite.toFinset hD) := by
  simp only [id_eq, Finite.mem_toFinset]
  exact he
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
he' : e ∈ hD.toFinset
⊢ e ≤ hD.toFinset.sup id

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
he' : e ∈ hD.toFinset
⊢ e ≤ hD.toFinset.sup id
Tactic:
apply Finset.le_sup he'
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ∈ hD.toFinset
Tactic:
simp only [id_eq, Finite.mem_toFinset]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ∈ D

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ∈ D
Tactic:
exact he
State after:
no goals