mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
f : α →ᵇ β
⊢ ⇑(nsmulRec 0 f) = 0 • ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
⊢ Integrable f μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
f : α →ᵇ β
n : ℕ
⊢ ⇑(nsmulRec (n + 1) f) = (n + 1) • ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
f : α →ᵇ R
n : ℕ
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ (fun x ↦ x ^ n) '' range ⇑f → ∀ ⦃y : R⦄, y ∈ (fun x ↦ x ^ n) '' range ⇑f → dist x y ≤ C
x y : α
⊢ f x ^ n ∈ (fun x ↦ x ^ n) '' range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
f : α →ᵇ R
n : ℕ
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ (fun x ↦ x ^ n) '' range ⇑f → ∀ ⦃y : R⦄, y ∈ (fun x ↦ x ^ n) '' range ⇑f → dist x y ≤ C
x y : α
⊢ f y ^ n ∈ (fun x ↦ x ^ n) '' range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ‖u (∑ i, v.equivFun e i • v i)‖₊ = ‖∑ i, v.equivFun e i • u (v i)‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
f : α →ᵇ R
n : ℕ
⊢ ∃ C, ∀ (x y : α), dist (f x ^ n) (f y ^ n) ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ∑ i, ‖v.equivFun e i • u (v i)‖₊ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
⊢ ∀ (x y : α →ᵇ R), (x * y).toContinuousMap = x.toContinuousMap * y.toContinuousMap

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
ι : Type u_3
s : Finset ι
inst✝² : CommMonoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
f : ι → α →ᵇ R
a : α
⊢ (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ ≤ ∑ i, ‖v.equivFun e i‖₊ * M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ ∑ i, ‖v.equivFun e i‖₊ * M = (∑ i, ‖v.equivFun e i‖₊) * M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ (∑ i, ‖v.equivFun e i‖₊) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
⊢ Tendsto F_lp l (𝓝 f_lp)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
⊢ ‖u e‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M * ‖e‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ LipschitzWith (LipschitzAdd.C β) fun p ↦ p.1 + p.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
hu : ∀ (i : ι), ‖u (v i)‖ ≤ M
⊢ ‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (f x) (f y) ≤ b
x y : α
⊢ dist ((c • f.toContinuousMap).toFun x) ((c • f.toContinuousMap).toFun y) ≤ dist c 0 * b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
this : Tendsto (fun i ↦ setToFun μ T hT ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT f))
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
⊢ dist (c • f₁) (c • f₂) ≤ dist c 0 * dist f₁ f₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ 0 ≤ dist c₁ c₂ * dist f 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
G : Type u_5
𝕜 : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ Tendsto (fun n ↦ setToFun μ T hT ⇑(SimpleFunc.approxOn f fmeas s 0 ⋯ n)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ dist (c₁ • f) (c₂ • f) ≤ dist c₁ c₂ * dist f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : SecondCountableTopology F
⊢ SecondCountableTopology (E →L[𝕜] F)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ f x ≤ nndist f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
h : ∀ (x : E), x ∈ F
⊢ ⊤ = F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
h : Nonempty α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ ‖f x‖ = dist (f x) (0 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
⊢ ∃ x, x ∉ F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f.normComp‖ = ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = ⨆ x, ‖f x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
inst✝² : Nonempty α
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 ↦ x1 • x2) (Int.ofNat n) f) = Int.ofNat n • ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 ↦ x1 • x2) (Int.negSucc n) f) = Int.negSucc n • ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
n : ℤ
f : α →ᵇ β
⊢ ∃ C, ∀ (x y : α), dist ((n • f.toContinuousMap).toFun x) ((n • f.toContinuousMap).toFun y) ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = ‖-f + g‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ⨆ x, ‖f x‖ = ↑(⨆ x, ‖f x‖₊)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ₑ = ⨆ x, ‖f x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
⊢ ‖f x - g x‖ ≤ dist f g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
⊢ ∀ y ∈ F, 1 ≤ ‖y - x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ ↑1 * dist f 0 ≤ ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g✝ ∘ ⇑(f + g)) ⋯ (‖g✝‖ * ‖f + g‖) ⋯ =
    ofNormedAddCommGroup (⇑g✝ ∘ ⇑f) ⋯ (‖g✝‖ * ‖f‖) ⋯ + ofNormedAddCommGroup (⇑g✝ ∘ ⇑g) ⋯ (‖g✝‖ * ‖g‖) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
⊢ ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g ∘ ⇑(c • f)) ⋯ (‖g‖ * ‖c • f‖) ⋯ =
    (RingHom.id 𝕜) c • ofNormedAddCommGroup (⇑g ∘ ⇑f) ⋯ (‖g‖ * ‖f‖) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x✝ : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : α →ᵇ β
x : α
⊢ ‖(⇑g ∘ ⇑f) x‖ ≤ ‖g‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
⊢ ∀ (x y : α →ᵇ β), (x + y).compContinuous g = x.compContinuous g + y.compContinuous g

Tactic:
by

Goal state after: