mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ ∀ (v : E), v ≠ 0 → (innerₗ E) v ≠ 0

pp: case refine_2
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ Continuous fun p ↦ ((innerₗ E) p.1) p.2

Tactic:
·

Goal state after:
case refine_1
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ ∀ (v : E), v ≠ 0 → (innerₗ E) v ≠ 0
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case refine_2
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ Continuous fun p ↦ ((innerₗ E) p.1) p.2

Tactic:
·

Goal state after:
case refine_2
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ Continuous fun p ↦ ((innerₗ E) p.1) p.2
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ ∫ (x : E), ∫ (y : E), cexp (↑⟪x + y, t⟫ * I) ∂ν ∂μ =
    (∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂μ) * ∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂ν

pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ Integrable (fun x ↦ cexp (↑⟪x, t⟫ * I)) (μ ∗ ν)

Tactic:
·

Goal state after:
E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ ∫ (x : E), ∫ (y : E), cexp (↑⟪x + y, t⟫ * I) ∂ν ∂μ =
    (∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂μ) * ∫ (x : E), cexp (↑⟪x, t⟫ * I) ∂ν
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ Integrable (fun x ↦ cexp (↑⟪x, t⟫ * I)) (μ ∗ ν)

Tactic:
·

Goal state after:
E : Type u_3
inst✝⁶ : MeasurableSpace E
μ ν : Measure E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
t : E
⊢ Integrable (fun x ↦ cexp (↑⟪x, t⟫ * I)) (μ ∗ ν)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ i, t i, _] (I'.attach.sup fs)

pp: case h.right.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ I'.attach.sup fs x = 0

pp: case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ

Tactic:
·

Goal state after:
case h.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ i, t i, _] (I'.attach.sup fs)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
n : Fin N
hn : n ∈ Finset.univ
⊢ ENNReal.ofReal (ε' / ↑N) ≠ ∞

Tactic:
·

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
n : Fin N
hn : n ∈ Finset.univ
⊢ ENNReal.ofReal (ε' / ↑N) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑x * I)) (Measure.map (⇑L) μ)

Tactic:
·

Goal state after:
case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑x * I)) (Measure.map (⇑L) μ)

Tactic:
·

Goal state after:
case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑x * I)) (Measure.map (⇑L) μ)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h.right.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ I'.attach.sup fs x = 0

pp: case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ

Tactic:
·

Goal state after:
case h.right.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ I'.attach.sup fs x = 0
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ

Tactic:
·

Goal state after:
case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), cexp (↑((u • L) x) * I) ∂μ = ∫ (x : E), cexp (↑u * ↑(L x) * I) ∂μ

pp: case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)

Tactic:
·

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), cexp (↑((u • L) x) * I) ∂μ = ∫ (x : E), cexp (↑u * ↑(L x) * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)

Tactic:
·

Goal state after:
case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)

Tactic:
·

Goal state after:
case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ 𝓝 x ≤ comap stoneCechUnit (𝓝 (stoneCechUnit x))

pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ comap stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x

Tactic:
·

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ 𝓝 x ≤ comap stoneCechUnit (𝓝 (stoneCechUnit x))
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ comap stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x

Tactic:
·

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ comap stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_1
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst✝] K
hx✝ : x ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Continuous[inst✝, _] (sᶜ.indicator 1)

pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
·

Goal state after:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst✝] K
hx✝ : x ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Continuous[inst✝, _] (sᶜ.indicator 1)
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
·

Goal state after:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x✝ : X
K : Set X
hK : IsClosed[inst✝] K
hx✝¹ : x✝ ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx✝ : x✝ ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case hbc.hb
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
⊢ 0 ≤ Λ (∑ x, g x)

pp: case hbc.h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
⊢ μ K ≤ ENNReal.ofReal (Λ (∑ x, g x))

Tactic:
·

Goal state after:
case hbc.hb
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
⊢ 0 ≤ Λ (∑ x, g x)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case hbc.h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
⊢ μ K ≤ ENNReal.ofReal (Λ (∑ x, g x))

Tactic:
·

Goal state after:
case hbc.h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := ⋯
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := ⋯
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
⊢ μ K ≤ ENNReal.ofReal (Λ (∑ x, g x))
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ x ∈ f ⁻¹' Iio r

pp: case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s

Tactic:
·

Goal state after:
case refine_1
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ x ∈ f ⁻¹' Iio r
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s

Tactic:
·

Goal state after:
case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: case mp
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)

pp: case mpr
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto id L (𝓝 x) → Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto diracProba L (𝓝 (diracProba x)) → Tendsto id L (𝓝 x)