mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : SeparableSpace α
⊢ SeparableSpace (Compacts α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝¹ : SeparableSpace (Compacts α)
h✝ : Nonempty α
s : Set (Compacts α)
hs₁ : s.Countable
hs₂ : Dense s
U : Set α
hU : IsOpen[inst✝] U
x✝ : U.Nonempty
x : α
hx : x ∈ U
⊢ {x} ∈ {K | ↑K ⊆ U} ∩ {K | (↑K ∩ U).Nonempty}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ SeparableSpace (Compacts α) ↔ SeparableSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ s} ⊆ {K | (↑K).Nonempty ∧ ↑K ⊆ s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected {K | (↑K).Nonempty ∧ ↑K ⊆ s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
hKL : K ≤ L
⊢ ContinuousOn (fun x ↦ K ⊔ x) {K | (↑K).Nonempty ∧ ↑K ⊆ ↑L}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
hK : K ≠ ⊥
hL : IsPreconnected ↑L
⊢ IsPreconnected (Icc K L)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
g : α →C₀ β
toFun✝ : α → β
continuous_toFun✝ : Continuous[inst✝⁴, inst✝³] toFun✝
zero_at_infty'✝ : Tendsto { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (cocompact α) (𝓝 0)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, continuous_toFun := continuous_toFun✝, zero_at_infty' := zero_at_infty'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝, zero_at_infty' := zero_at_infty'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous[inst✝⁴, inst✝³] toFun✝¹
zero_at_infty'✝¹ : Tendsto { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun (cocompact α) (𝓝 0)
toFun✝ : α → β
continuous_toFun✝ : Continuous[inst✝⁴, inst✝³] toFun✝
zero_at_infty'✝ : Tendsto { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (cocompact α) (𝓝 0)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, continuous_toFun := continuous_toFun✝, zero_at_infty' := zero_at_infty'✝ }
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝, zero_at_infty' := zero_at_infty'✝ }
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
⊢ ∀ u ∈ {s | IsOpen s ∧ IsPreconnected s}, IsOpen u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Continuous[inst✝⁴, inst✝³] f'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : α →C₀ β
f' : α → β
h : f' = ⇑f
⊢ Tendsto f' (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroAtInftyContinuousMapClass F α β
inst✝ : CompactSpace α
f : C(α, β)
⊢ Tendsto (⇑f) (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero β
G : Type u_2
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), Tendsto (⇑f) (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : MulZeroClass β
inst✝ : ContinuousMul β
f g : α →C₀ β
⊢ Tendsto (↑f * ↑g).toFun (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
U : Set (Compacts α)
hU :
  U ∈
    (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}}
this : IsPreconnected (U ∩ {K | (↑K).Finite})
⊢ IsPreconnected U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
f g : α →C₀ β
⊢ Tendsto (↑f + ↑g).toFun (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
x : α
inst✝³ : Zero β
R : Type u_2
inst✝² : Zero R
inst✝¹ : SMulWithZero R β
inst✝ : ContinuousConstSMul R β
r : R
f : α →C₀ β
⊢ Tendsto (r • ↑f).toFun (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g f : α →C₀ β
⊢ Tendsto (-↑f).toFun (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g✝ f g : α →C₀ β
⊢ Tendsto (↑f - ↑g).toFun (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : IsScalarTower R β β
r : R
f g : α →C₀ β
⊢ (r • f) • g = r • f • g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
⊢ r • f • g = f • r • g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ ContinuousOn Finset.univ.sup (univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this✝ : Fintype ↑u := hu'.fintype
this :
  {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite} =
    Finset.univ.sup '' univ.pi fun U ↦ {K | (↑K).Nonempty ∧ (↑K).Finite ∧ ↑K ⊆ ↑U}
⊢ IsPreconnected {a | ↑a ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑a ∩ U).Nonempty) ∧ (↑a).Finite}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1
C : ℝ
hC : ⇑f '' K ⊆ closedBall 0 C
x y : α
⊢ ∀ (x : α), f x ∈ closedBall 0 (max C 1)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s = ⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed[WeakBilin.instTopologicalSpace B.flip] (B.polar s)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ‖(B x✝¹) 0‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ (B.polar s).Nonempty

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s = ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
⊢ ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ expMulMulExp a b x z = ↑(expUnitary (2 • ℑ (z • star b))) * x * ↑(expUnitary (2 • ℑ (star z • a)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
⊢ f = g

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy : y ∈ {y | ‖(B a) y‖ ≤ 1}
x✝ : E
hb : x✝ ∈ {a}
⊢ ‖(B x✝) y‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i ↦ ⇑(F i)) (⇑f) l

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ Differentiable ℂ (expMulMulExp a b x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
⊢ Isometry toBCF

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
x : E
y : F
⊢ y ∈ B.polar {x} ↔ ‖(B x) y‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ B.polar {0} = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyConnectedSpace α
basis :
  IsTopologicalBasis
    ((fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) ''
      {u | u.Finite ∧ u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}})
u : Set (Set α)
hu' : u.Finite
hu : u ⊆ {s | IsOpen[inst✝³] s ∧ IsPreconnected s}
this : Fintype ↑u := hu'.fintype
K : Compacts α
x✝ : K ∈ {K | ↑K ⊆ ⋃₀ u ∧ (∀ U ∈ u, (↑K ∩ U).Nonempty) ∧ (↑K).Finite}
hK₁ : ↑K ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
hK₃ : (↑K).Finite
⊢ (Finset.univ.sup fun U ↦ { carrier := ↑K ∩ ↑U, isCompact' := ⋯ }) = K

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B.flip y) x‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
hf : Differentiable ℂ (expMulMulExp a b x)
⊢ IsBounded (Set.range (expMulMulExp a b x))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
⊢ expMulMulExp a b x z = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a✝ b x : A
inst✝¹ : IsStarNormal a✝
inst✝ : IsStarNormal b
h : SemiconjBy x a✝ b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a✝) = NormedSpace.exp (z • star b) * x
a : A
⊢ HasDerivAt (fun z ↦ NormedSpace.exp (z • a)) a 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) = B.polar s

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ 0 ∈ B.polar Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
key : ∀ (z : ℂ), x * NormedSpace.exp (z • star a) = NormedSpace.exp (z • star b) * x
⊢ SemiconjBy x (star a) (star b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty
ε : ℝ
hε : ε > 0
g : α →C₀ β
hg : g.toBCF ∈ ball f (ε / 2)
x : α
hx : dist (g x) 0 < ε / 2
⊢ dist g.toBCF f + ε / 2 ≤ ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →ᵇ β
hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty
⊢ Tendsto (⇑f) (cocompact α) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy x (star a) (star b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
⊢ IsClosed (range toBCF)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_2
inst✝ : NonUnitalCStarAlgebra A
a b x : A
ha : IsStarNormal a
hb : IsStarNormal b
h : SemiconjBy x a b
⊢ SemiconjBy x (star a) (star b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C₀ β
⊢ Tendsto (fun x ↦ star (f x)) (cocompact α) (𝓝 0)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖(B x) y‖ = ‖c‖ * ‖(B (c⁻¹ • x)) y‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : y ∈ B.polar Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖c‖ * ‖(B (c⁻¹ • x)) y‖ ≤ ε * 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
⊢ B.polar Set.univ = {0}

Tactic:
by

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

Goal state before:
pp: E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) s)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
x : E
⊢ x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ (absConvexHull 𝕜) s = ∅ ↔ s = ∅

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : SMul 𝕜 E
inst✝² : AddCommMonoid E
inst✝¹ : PartialOrder 𝕜
inst✝ : TopologicalSpace E
s : Set E
⊢ (closedAbsConvexHull 𝕜) (closure[inst✝] s) ⊆ (closedAbsConvexHull 𝕜) s

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
⊢ B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
⊢ B.polar ↑m = ↑(⨅ x ∈ m, (B x).ker)

Tactic:
by

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝³ : SeminormedCommRing R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (topDualPairing R M).SeparatingLeft

Tactic:
by

Goal state after: