internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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'
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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]
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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)
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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'
Proof state after:
no goals
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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'
Proof state after:
no goals
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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]
Proof 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
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof 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
Proof state after:
no goals
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ⊓ basis σ α e
Tactic:
simp_rw [le_inf_iff]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ∧ basis σ α k ≤ basis σ α e
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ∧ basis σ α k ≤ basis σ α e
Tactic:
exact ⟨d + e, basis_antitone _ _ (le_self_add), basis_antitone _ _ (le_add_self)⟩
Proof state after:
no goals
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ᶠ (a : MvPowerSeries σ α) in nhds 0, a • f ∈ basis σ α d
Tactic:
rw [Filter.eventually_iff_exists_mem]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∃ v ∈ nhds 0, ∀ y ∈ v, y • f ∈ basis σ α d
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∃ v ∈ nhds 0, ∀ y ∈ v, y • f ∈ basis σ α d
Tactic:
refine ⟨↑(basis σ α d), (basis_mem_nhds_zero σ α d), ?_⟩
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ y ∈ ↑(basis σ α d), y • f ∈ basis σ α d
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ y ∈ ↑(basis σ α d), y • f ∈ basis σ α d
Tactic:
intros g hg
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ g • f ∈ basis σ α d
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ g • f ∈ basis σ α d
Tactic:
rw [smul_eq_mul, mul_comm]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ f * g ∈ basis σ α d
Theorem: MvPowerSeries.toSubmodulesBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ f * g ∈ basis σ α d
Tactic:
exact Ideal.mul_mem_left _ f (SetLike.mem_coe.mp hg)
Proof state after:
no goals
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
⊢ U ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ U
Tactic:
let τ := MvPowerSeries.WithPiTopology.topologicalSpace σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ U ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ U
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ U ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ U
Tactic:
constructor
Proof state after:
case mp
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ U ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ U

case mpr
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ (∃ i, {b | b ∈ basis σ α i} ⊆ U) → U ∈ nhds 0
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case mp
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ U ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ U
Tactic:
rw [nhds_pi, Filter.mem_pi]
Proof state after:
case mp
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ U) → ∃ i, {b | b ∈ basis σ α i} ⊆ U
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case mp
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ U) → ∃ i, {b | b ∈ basis σ α i} ⊆ U
Tactic:
rintro ⟨D, hD, t, ht, ht'⟩
Proof state after:
case mp.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ U
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case mp.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ U
Tactic:
use Finset.sup hD.toFinset id
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ U
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ U
Tactic:
apply subset_trans _ ht'
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ D.pi t
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ D.pi t
Tactic:
intros f hf e he
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ f e ∈ t e
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
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]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
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 α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ 0 ∈ t e
Tactic:
exact mem_of_mem_nhds (ht e)
Proof state after:
no goals
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ e ≤ hD.toFinset.sup id
Tactic:
rw [← id_eq e]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ id e ≤ hD.toFinset.sup id
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ U
f : (σ →₀ ℕ) → α
hf : f ∈ {b | b ∈ basis σ α (hD.toFinset.sup id)}
e : σ →₀ ℕ
he : e ∈ D
⊢ id e ≤ hD.toFinset.sup id
Tactic:
exact Finset.le_sup ((Set.Finite.mem_toFinset _).mpr he)
Proof state after:
no goals
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case mpr
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ (∃ i, {b | b ∈ basis σ α i} ⊆ U) → U ∈ nhds 0
Tactic:
rintro ⟨d, hd⟩
Proof state after:
case mpr.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
d : σ →₀ ℕ
hd : {b | b ∈ basis σ α d} ⊆ U
⊢ U ∈ nhds 0
Theorem: MvPowerSeries.mem_nhds_zero_iff
Proof state before:
case mpr.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
U : Set (MvPowerSeries σ α)
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
d : σ →₀ ℕ
hd : {b | b ∈ basis σ α d} ⊆ U
⊢ U ∈ nhds 0
Tactic:
exact (@nhds _ τ 0).sets_of_superset (basis_mem_nhds_zero σ α d) hd
Proof state after:
no goals
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ := MvPowerSeries.WithPiTopology.topologicalSpace σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ' := (toSubmodulesBasis σ α).topology
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
rw [TopologicalAddGroup.ext_iff_nhds_zero τ τ']
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0