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
⊢ ⋂ d, {p | φ (p ↑d) ∈ I} ∈ nhds 0 ∧ toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I} ⊆ eval₂ φ a ⁻¹' u
Tactic:
rw [nhds_pi, Filter.mem_pi]
Proof state after:
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_1, I_1.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I_1.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}) ∧
    toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I} ⊆ eval₂ φ a ⁻¹' u
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_1, I_1.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I_1.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}) ∧
    toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I} ⊆ eval₂ φ a ⁻¹' u
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_1, I_1.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I_1.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ 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
⊢ toMvPowerSeries ⁻¹' ⋂ d, {p | φ (p ↑d) ∈ I} ⊆ eval₂ φ a ⁻¹' u
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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}
s : σ
⊢ {n | a s ^ n.succ ∈ I}.Nonempty
Tactic:
rcases hpow' s with ⟨n, hn⟩
Proof state after:
case intro
σ : 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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ {n | a s ^ n.succ ∈ I}.Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case intro
σ : 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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ {n | a s ^ n.succ ∈ I}.Nonempty
Tactic:
use n
Proof state after:
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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ n ∈ {n | a s ^ n.succ ∈ I}
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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ n ∈ {n | a s ^ n.succ ∈ I}
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ a s ^ n.succ ∈ I
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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ I
⊢ a s ^ n.succ ∈ I
Tactic:
refine hn n.succ (Nat.le_succ n)
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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
⊢ (Function.support n).Finite
Tactic:
apply @Finite.Set.subset  _ _ _ tendsto_zero
Proof state after:
σ : 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
⊢ Function.support n ⊆ (a ⁻¹' ↑I)ᶜ
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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
⊢ Function.support n ⊆ (a ⁻¹' ↑I)ᶜ
Tactic:
intro s
Proof state after:
σ : 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
s : σ
⊢ s ∈ Function.support n → s ∈ (a ⁻¹' ↑I)ᶜ
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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
s : σ
⊢ s ∈ Function.support n → s ∈ (a ⁻¹' ↑I)ᶜ
Tactic:
simp only [Function.mem_support, ne_eq, Set.mem_compl_iff, Set.mem_preimage, SetLike.mem_coe, not_imp_comm, not_not]
Proof state after:
σ : 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
s : σ
⊢ a s ∈ I → n s = 0
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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
s : σ
⊢ a s ∈ I → n s = 0
Tactic:
simp only [imp_or, n, Nat.sInf_eq_zero, Set.mem_setOf_eq, zero_add, pow_one, imp_self, true_or]
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : 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
s : σ
⊢ s ∈ hn.toFinset ↔ n s ≠ 0
Tactic:
simp
Proof state after:
no goals
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_1, I_1.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I_1.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Tactic:
use D, hD
Proof state after:
case 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
⊢ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ D.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case 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
⊢ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ D.pi t ⊆ ⋂ d, {p | φ (p ↑d) ∈ I}
Tactic:
use fun d ↦ if d ∈ D then φ ⁻¹' I else Set.univ
Proof state after:
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}