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

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 σ α
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

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
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

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]
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

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'⟩
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

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
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

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'
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

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
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

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]
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

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)
State after:
no goals

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]
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

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)
State after:
no goals

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⟩
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

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
State after:
no goals