Borel (measurable) space #

Main definitions #

borel α : the least σ-algebra that contains all open sets;
class BorelSpace : a space with TopologicalSpace and MeasurableSpace structures such that ‹MeasurableSpace α› = borel α;
class OpensMeasurableSpace : a space with TopologicalSpace and MeasurableSpace structures such that all open sets are measurable; equivalently, borel α ≤ ‹MeasurableSpace α›.
BorelSpace instances on Empty, Unit, Bool, Nat, Int, Rat;
MeasurableSpace and BorelSpace instances on ℝ, ℝ≥0, ℝ≥0∞.

Main statements #

IsOpen.measurableSet, IsClosed.measurableSet: open and closed sets are measurable;
Continuous.measurable : a continuous function is measurable;
Continuous.measurable2 : if f : α → β and g : α → γ are measurable and op : β × γ → δ is continuous, then fun x => op (f x, g y) is measurable;
Measurable.add etc : dot notation for arithmetic operations on Measurable predicates, and similarly for dist and edist;
AEMeasurable.add : similar dot notation for almost everywhere measurable functions;

source

def borel (α : Type u) [TopologicalSpace α] :

MeasurableSpace α

MeasurableSpace structure generated by TopologicalSpace.

Equations

borel α = MeasurableSpace.generateFrom {s : Set α | IsOpen s}

source

theorem borel_anti {α : Type u_1} :

Antitone (@borel α)

source

theorem borel_eq_top_of_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] :

borel α = ⊤

source

theorem borel_eq_generateFrom_of_subbasis {α : Type u_1} {s : Set (Set α)} [t : TopologicalSpace α] [SecondCountableTopology α] (hs : t = TopologicalSpace.generateFrom s) :

borel α = MeasurableSpace.generateFrom s

source

theorem TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] {s : Set (Set α)} (hs : IsTopologicalBasis s) :

borel α = MeasurableSpace.generateFrom s

source

theorem isPiSystem_isOpen {α : Type u_1} [TopologicalSpace α] :

IsPiSystem {s : Set α | IsOpen s}

source

theorem isPiSystem_isClosed {α : Type u_1} [TopologicalSpace α] :

IsPiSystem {s : Set α | IsClosed s}

source

theorem borel_eq_generateFrom_isClosed {α : Type u_1} [TopologicalSpace α] :

borel α = MeasurableSpace.generateFrom {s : Set α | IsClosed s}

source

theorem borel_comap {α : Type u_1} {β : Type u_2} {f : α → β} {t : TopologicalSpace β} :

borel α = MeasurableSpace.comap f (borel β)

source

theorem Continuous.borel_measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) :

Measurable f

source

class OpensMeasurableSpace (α : Type u_6) [TopologicalSpace α] [h : MeasurableSpace α] :

Prop

A space with MeasurableSpace and TopologicalSpace structures such that all open sets are measurable.

borel_le : borel α ≤ h
Borel-measurable sets are measurable.

Instances

source

class BorelSpace (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] :

Prop

A space with MeasurableSpace and TopologicalSpace structures such that the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.

measurable_eq : inst✝ = borel α
The measurable sets are exactly the Borel-measurable sets.

Instances

source

def Mathlib.Tactic.Borelize.tacticBorelize___ :

Lean.ParserDescr

The behaviour of borelize α depends on the existing assumptions on α.

if α is a topological space with instances [MeasurableSpace α] [BorelSpace α], then borelize α replaces the former instance by borel α;
otherwise, borelize α adds instances borel α : MeasurableSpace α and ⟨rfl⟩ : BorelSpace α.

Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

Equations

One or more equations did not get rendered due to their size.

source

def Mathlib.Tactic.Borelize.addBorelInstance (e : Lean.Expr) :

Lean.Elab.Tactic.TacticM Unit

Add instances borel e : MeasurableSpace e and ⟨rfl⟩ : BorelSpace e.

Equations

One or more equations did not get rendered due to their size.

source

def Mathlib.Tactic.Borelize.borelToRefl (e : Lean.Expr) (i : Lean.FVarId) :

Lean.Elab.Tactic.TacticM Unit

Given a type e, an assumption i : MeasurableSpace e, and an instance [BorelSpace e], replace i with borel e.

Equations

One or more equations did not get rendered due to their size.

source

def Mathlib.Tactic.Borelize.borelize (t : Lean.Term) :

Lean.Elab.Tactic.TacticM Unit

Given a type $t, if there is an assumption [i : MeasurableSpace $t], then try to prove [BorelSpace $t] and replace i with borel $t. Otherwise, add instances borel $t : MeasurableSpace $t and ⟨rfl⟩ : BorelSpace $t.

Equations

One or more equations did not get rendered due to their size.

source

@[instance 100]

instance OrderDual.opensMeasurableSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : OpensMeasurableSpace α] :

OpensMeasurableSpace αᵒᵈ

source

@[instance 100]

instance OrderDual.borelSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : BorelSpace α] :

BorelSpace αᵒᵈ

source

@[instance 100]

instance BorelSpace.opensMeasurable {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] :

OpensMeasurableSpace α

In a BorelSpace all open sets are measurable.

source

instance Subtype.borelSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [hα : BorelSpace α] (s : Set α) :

BorelSpace ↑s

source

instance Countable.instBorelSpace {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace α] [DiscreteTopology α] :

BorelSpace α

source

instance Subtype.opensMeasurableSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : OpensMeasurableSpace α] (s : Set α) :

OpensMeasurableSpace ↑s

source

theorem opensMeasurableSpace_iff_forall_measurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] :

OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s

source

@[instance 100]

instance BorelSpace.countablyGenerated {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] :

MeasurableSpace.CountablyGenerated α

source

theorem IsOpen.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsOpen s) :

MeasurableSet s

source

theorem IsOpen.nullMeasurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} (h : IsOpen s) :

MeasureTheory.NullMeasurableSet s μ

source

theorem MeasurableSet.induction_on_open {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {C : (s : Set γ) → MeasurableSet s → Prop} (isOpen : ∀ (U : Set γ) (hU : IsOpen U), C U ⋯) (compl : ∀ (t : Set γ) (ht : MeasurableSet t), C t ht → C tᶜ ⋯) (iUnion : ∀ (f : ℕ → Set γ), Pairwise (Function.onFun Disjoint f) → ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯) (t : Set γ) (ht : MeasurableSet t) :

C t ht

source

instance instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} [h : HasCountableSeparatingOn α IsOpen s] :

MeasurableSpace.CountablySeparated ↑s

source

theorem measurableSet_interior {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] :

MeasurableSet (interior s)

source

theorem IsGδ.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsGδ s) :

MeasurableSet s

source

theorem measurableSet_of_continuousAt {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {β : Type u_6} [PseudoEMetricSpace β] (f : α → β) :

MeasurableSet {x : α | ContinuousAt f x}

source

theorem IsClosed.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsClosed s) :

MeasurableSet s

source

theorem IsClosed.nullMeasurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} (h : IsClosed s) :

MeasureTheory.NullMeasurableSet s μ

source

theorem IsCompact.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T2Space α] (h : IsCompact s) :

MeasurableSet s

source

theorem IsCompact.nullMeasurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T2Space α] {μ : MeasureTheory.Measure α} (h : IsCompact s) :

MeasureTheory.NullMeasurableSet s μ

source

theorem Inseparable.mem_measurableSet_iff {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {x y : γ} (h : Inseparable x y) {s : Set γ} (hs : MeasurableSet s) :

x ∈ s ↔ y ∈ s

If two points are topologically inseparable, then they can't be separated by a Borel measurable set.

source

theorem IsCompact.closure_subset_measurableSet {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K s : Set γ} (hK : IsCompact K) (hs : MeasurableSet s) (hKs : K ⊆ s) :

closure K ⊆ s

If K is a compact set in an R₁ space and s ⊇ K is a Borel measurable superset, then s includes the closure of K as well.

source

theorem IsCompact.measure_closure {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : MeasureTheory.Measure γ) :

μ (closure K) = μ K

In an R₁ topological space with Borel measure μ, the measure of the closure of a compact set K is equal to the measure of K.

See also MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact for a version that assumes μ to be outer regular but does not assume the σ-algebra to be Borel.

source

theorem measurableSet_closure {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] :

MeasurableSet (closure s)

source

theorem measurable_of_isOpen {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)) :

Measurable f

source

theorem measurable_of_isClosed {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)) :

Measurable f

source

theorem measurable_of_isClosed' {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ Set.univ → MeasurableSet (f ⁻¹' s)) :

Measurable f

source

instance nhds_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (a : α) :

(nhds a).IsMeasurablyGenerated

source

theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (a : α) :

(nhdsWithin a s).IsMeasurablyGenerated

If s is a measurable set, then 𝓝[s] a is a measurably generated filter for each a. This cannot be an instance because it depends on a non-instance hs : MeasurableSet s.

source

@[instance 100]

instance OpensMeasurableSpace.separatesPoints {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T0Space α] :

MeasurableSpace.SeparatesPoints α

source

theorem borel_eq_top_of_countable {α : Type u_6} [TopologicalSpace α] [T0Space α] [Countable α] :

borel α = ⊤

source

@[instance 100]

instance OpensMeasurableSpace.toMeasurableSingletonClass {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T1Space α] :

MeasurableSingletonClass α

source

instance Pi.opensMeasurableSpace {ι : Type u_6} {X : ι → Type u_7} [Countable ι] [t' : (i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), OpensMeasurableSpace (X i)] :

OpensMeasurableSpace ((i : ι) → X i)

source

class SecondCountableTopologyEither (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] :

Prop

The typeclass SecondCountableTopologyEither α β registers the fact that at least one of the two spaces has second countable topology. This is the right assumption to ensure that continuous maps from α to β are strongly measurable.

out : SecondCountableTopology α ∨ SecondCountableTopology β
The projection out of SecondCountableTopologyEither

Instances

source

@[instance 100]

instance secondCountableTopologyEither_of_left (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology α] :

SecondCountableTopologyEither α β

source

@[instance 100]

instance secondCountableTopologyEither_of_right (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] :

SecondCountableTopologyEither α β

source

instance Prod.opensMeasurableSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [h : SecondCountableTopologyEither α β] :

OpensMeasurableSpace (α × β)

If either α or β has second-countable topology, then the open sets in α × β belong to the product sigma-algebra.

source

theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :

interior s =ᵐ[μ] s

source

theorem measure_interior_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :

μ (interior s) = μ s

source

theorem nullMeasurableSet_of_null_frontier {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : μ (frontier s) = 0) :

MeasureTheory.NullMeasurableSet s μ

source

theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :

closure s =ᵐ[μ] s

source

theorem measure_closure_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :

μ (closure s) = μ s

source

instance separatesPointsOfOpensMeasurableSpaceOfT0Space {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T0Space α] :

MeasurableSpace.SeparatesPoints α

source

theorem Continuous.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (hf : Continuous f) :

Measurable f

A continuous function from an OpensMeasurableSpace to a BorelSpace is measurable.

source

theorem Continuous.aemeasurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (h : Continuous f) {μ : MeasureTheory.Measure α} :

AEMeasurable f μ

A continuous function from an OpensMeasurableSpace to a BorelSpace is ae-measurable.

source

theorem IsClosedEmbedding.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (hf : Topology.IsClosedEmbedding f) :

Measurable f

source

@[deprecated IsClosedEmbedding.measurable (since := "2024-10-20")]

theorem ClosedEmbedding.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (hf : Topology.IsClosedEmbedding f) :

Measurable f

Alias of IsClosedEmbedding.measurable.

source

theorem ContinuousOn.measurable_piecewise {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f g : α → γ} {s : Set α} [(j : α) → Decidable (j ∈ s)] (hf : ContinuousOn f s) (hg : ContinuousOn g sᶜ) (hs : MeasurableSet s) :

Measurable (s.piecewise f g)

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

source

@[instance 100]

instance ContinuousMul.measurableMul {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Mul γ] [ContinuousMul γ] :

MeasurableMul γ

source

@[instance 100]

instance ContinuousAdd.measurableAdd {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Add γ] [ContinuousAdd γ] :

MeasurableAdd γ

source

@[instance 100]

instance ContinuousSub.measurableSub {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Sub γ] [ContinuousSub γ] :

MeasurableSub γ

source

@[instance 100]

instance ContinuousInv.measurableInv {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Inv γ] [ContinuousInv γ] :

MeasurableInv γ

source

@[instance 100]

instance ContinuousNeg.measurableNeg {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Neg γ] [ContinuousNeg γ] :

MeasurableNeg γ

source

@[instance 100]

instance ContinuousSMul.measurableSMul {M : Type u_7} {α : Type u_8} [TopologicalSpace M] [TopologicalSpace α] [MeasurableSpace M] [MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [SMul M α] [ContinuousSMul M α] :

MeasurableSMul M α

source

@[instance 100]

instance ContinuousVAdd.measurableVAdd {M : Type u_7} {α : Type u_8} [TopologicalSpace M] [TopologicalSpace α] [MeasurableSpace M] [MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [VAdd M α] [ContinuousVAdd M α] :

MeasurableVAdd M α

source

theorem Homeomorph.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] (h : α ≃ₜ γ) :

Measurable ⇑h

source

def Homeomorph.toMeasurableEquiv {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :

γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations

h.toMeasurableEquiv = { toEquiv := h.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

source

theorem Homeomorph.measurableEmbedding {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :

MeasurableEmbedding ⇑h

source

@[simp]

theorem Homeomorph.toMeasurableEquiv_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :

⇑h.toMeasurableEquiv = ⇑h

source

@[simp]

theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) :

⇑h.toMeasurableEquiv.symm = ⇑h.symm

source

theorem ContinuousMap.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] (f : C(α, γ)) :

Measurable ⇑f

source

theorem measurable_of_continuousOn_compl_singleton {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [T1Space α] {f : α → γ} (a : α) (hf : ContinuousOn f {a}ᶜ) :

Measurable f

source

theorem Continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : Measurable f) (hg : Measurable g) :

Measurable fun (a : δ) => c (f a) (g a)

source

theorem Continuous.aemeasurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : MeasureTheory.Measure δ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :

AEMeasurable (fun (a : δ) => c (f a) (g a)) μ

source

@[instance 100]

instance HasContinuousInv₀.measurableInv {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [GroupWithZero γ] [T1Space γ] [HasContinuousInv₀ γ] :

MeasurableInv γ

source

@[instance 100]

instance ContinuousMul.measurableMul₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Mul γ] [ContinuousMul γ] :

MeasurableMul₂ γ

source

@[instance 100]

instance ContinuousAdd.measurableMul₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Add γ] [ContinuousAdd γ] :

MeasurableAdd₂ γ

source

@[instance 100]

instance ContinuousSub.measurableSub₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Sub γ] [ContinuousSub γ] :

MeasurableSub₂ γ

source

@[instance 100]

instance ContinuousSMul.measurableSMul₂ {M : Type u_7} {α : Type u_8} [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M] [TopologicalSpace α] [SecondCountableTopologyEither M α] [MeasurableSpace α] [BorelSpace α] [SMul M α] [ContinuousSMul M α] :

MeasurableSMul₂ M α

source

theorem pi_le_borel_pi {ι : Type u_6} {X : ι → Type u_7} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), BorelSpace (X i)] :

MeasurableSpace.pi ≤ borel ((i : ι) → X i)

source

theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] :

Prod.instMeasurableSpace ≤ borel (α × β)

source

instance Pi.borelSpace {ι : Type u_6} {X : ι → Type u_7} [Countable ι] [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), BorelSpace (X i)] :

BorelSpace ((i : ι) → X i)

source