mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x = b • x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
he : ↑s₁ ∩ ↑s₂ = ∅
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
⊢ b • x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹ • r‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
⊢ Balanced 𝕜 (balancedCoreAux 𝕜 s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : Convex R s
⊢ Convex A s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
⊢ t ⊆ balancedCoreAux 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
⊢ Balanced 𝕜 (insert 0 (interior A))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (interior A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
⊢ (↑s₁ ∩ ↑s₂).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ Balanced 𝕜 ((convexHull 𝕜) s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ balancedCore 𝕜 t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ → q = p

Tactic:
rintro ⟨hq1, hq2⟩
    have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction :=
      ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
    rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s = s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
d₁ d₂ : Submodule k V
⊢ mk' p d₁ ≤ mk' p d₂ ↔ d₁ ≤ d₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s = ⊥ ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ⊥ < affineSpan k s ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
⊢ Balanced 𝕜 ((convexHull 𝕜) s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∉ U
⊢ balancedCore 𝕜 U = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
⊢ ↑V = univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ p x h

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ line[k, p₁, p₂] ≤ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
⊢ ∀ (i : 𝕜), ‖i‖ ≤ 1 ∧ i ≠ 0 → ∃ i', ∃ (_ : ‖i'‖ ≤ 1), i • s ⊆ i' • s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Balanced ℝ s
x✝ : E
hx : x✝ ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ ‖a‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
hr : ‖0‖ ≤ 1
⊢ ‖1‖ ≤ 1 ∧ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
hr : ‖0‖ ≤ 1
⊢ 0 • s ⊆ 1 • s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ affineSpan k (insert p ps) = affineSpan k ps

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ vectorSpan k (insert p ps) = vectorSpan k ps

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
⊢ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s = ⋃ r, ⋃ (_ : ‖r‖ ≤ 1 ∧ r ≠ 0), r • s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ affineSpan k s ≤ ↑(Submodule.span k s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
⊢ IsOpen[inst✝¹] (balancedHull 𝕜 s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s ∧ Balanced 𝕜 s) id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
s t : Set E
⊢ IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : SMul 𝕜 E
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ι : Sort u_6
inst✝ : Finite ι
s : ι → Set E
⊢ IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddZeroClass E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U (s + t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U (-s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s - t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ Tendsto (fun x ↦ x • S) (𝓝 0) (𝓝 0).smallSets

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ map (⇑σ) (𝓝 0) = 𝓝 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
⊢ ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ IsVonNBounded 𝕜 S

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : Tendsto ε l (𝓝[≠] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ ∃ ε, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
⊢ ∀ᶠ (n : ℕ) in ?m.101, ε n • 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕝 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
⊢ IsVonNBounded 𝕜 (closure[inst✝³] a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
x : E
s : Set E
⊢ IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (x +ᵥ s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
x : E
h : IsVonNBounded 𝕜 (x +ᵥ s)
⊢ IsVonNBounded 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : IsTopologicalAddGroup E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
by

Goal state after: