internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ (∀ (i : σ →₀ ℕ), (if i ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ∈ nhds (0 i)) ∧
    (D.pi fun d => if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Tactic:
constructor
Proof state after:
case h.left
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ ∀ (i : σ →₀ ℕ), (if i ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ∈ nhds (0 i)

case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ (D.pi fun d => if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.left
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ ∀ (i : σ →₀ ℕ), (if i ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ∈ nhds (0 i)
Tactic:
intro d
Proof state after:
case h.left
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
⊢ (if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ∈ nhds (0 d)
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.left
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
⊢ (if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ∈ nhds (0 d)
Tactic:
split_ifs with hd
Proof state after:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ⇑φ ⁻¹' ↑I ∈ nhds (0 d)

case neg
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∉ D
⊢ Set.univ ∈ nhds (0 d)
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ⇑φ ⁻¹' ↑I ∈ nhds (0 d)
Tactic:
apply hφ.continuousAt.preimage_mem_nhds
Proof state after:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ↑I ∈ nhds (φ (0 d))
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ↑I ∈ nhds (φ (0 d))
Tactic:
erw [RingHom.map_zero]
Proof state after:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ↑I ∈ nhds 0
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case pos
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ↑I ∈ nhds 0
Tactic:
exact hI
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∉ D
⊢ Set.univ ∈ nhds (0 d)
Tactic:
exact Filter.univ_mem
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ (D.pi fun d => if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Tactic:
intro p
Proof state after:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : (σ →₀ ℕ) → R
⊢ (p ∈ D.pi fun d => if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) → p ∈ ⋂ d, {p | φ (p ↑d) ∈ I}
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : (σ →₀ ℕ) → R
⊢ (p ∈ D.pi fun d => if d ∈ D then ⇑φ ⁻¹' ↑I else Set.univ) → p ∈ ⋂ d, {p | φ (p ↑d) ∈ I}
Tactic:
simp only [Set.mem_pi, Set.mem_ite_univ_right, Set.mem_preimage, SetLike.mem_coe,
  Set.iInter_coe_set, Set.mem_iInter]
Proof state after:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : (σ →₀ ℕ) → R
⊢ (∀ i ∈ D, i ∈ D → φ (p i) ∈ I) → ∀ i ∈ D, p ∈ {p | φ (p i) ∈ I}
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : (σ →₀ ℕ) → R
⊢ (∀ i ∈ D, i ∈ D → φ (p i) ∈ I) → ∀ i ∈ D, p ∈ {p | φ (p i) ∈ I}
Tactic:
exact fun hp i hi ↦ hp i hi hi
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
⊢ toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I} ⊆ eval₂ φ a ⁻¹' u
Tactic:
intro p hp
Proof state after:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : p ∈ toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I}
⊢ p ∈ eval₂ φ a ⁻¹' u
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : p ∈ toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I}
⊢ p ∈ eval₂ φ a ⁻¹' u
Tactic:
simp only [Set.iInter_coe_set, Set.mem_preimage, coeToMvPowerSeries.ringHom_apply,
  Set.mem_iInter, Set.mem_setOf_eq] at hp
Proof state after:
case h.right
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (↑p i) ∈ I
⊢ p ∈ eval₂ φ a ⁻¹' u