# Measurable spaces and measurable functions #

This file defines measurable spaces and measurable functions.

A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.

σ-algebras on a fixed set `α` form a complete lattice. Here we order σ-algebras by writing `m₁ ≤ m₂` if every set which is `m₁`-measurable is also `m₂`-measurable (that is, `m₁` is a subset of `m₂`). In particular, any collection of subsets of `α` generates a smallest σ-algebra which contains all of them.

## References #

- https://en.wikipedia.org/wiki/Measurable_space
- https://en.wikipedia.org/wiki/Sigma-algebra
- https://en.wikipedia.org/wiki/Dynkin_system

## Tags #

measurable space, σ-algebra, measurable function

source
class MeasurableSpace (α : Type u_7) :
Type u_7

A measurable space is a space equipped with a σ-algebra.

- MeasurableSet' : Set α → Prop

  Predicate saying that a given set is measurable. Use `MeasurableSet` in the root namespace instead.

- measurableSet_empty : MeasurableSet' self ∅

  The empty set is a measurable set. Use `MeasurableSet.empty` instead.

- measurableSet_compl (s : Set α) : MeasurableSet' self s → MeasurableSet' self s ᶜ

  The complement of a measurable set is a measurable set. Use `MeasurableSet.compl` instead.

- measurableSet_iUnion (f : ℕ → Set α) : (∀ (i : ℕ), MeasurableSet' self (f i)) → MeasurableSet' self (⋃ (i : ℕ), f i)

  The union of a sequence of measurable sets is a measurable set. Use a more general `MeasurableSet.iUnion` instead.

Instances

source
instance instMeasurableSpaceOrderDual {α : Type u_1} [h : MeasurableSpace α] :
MeasurableSpace α ᵒᵈ
Equations

- instMeasurableSpaceOrderDual = h

source
def MeasurableSet {α : Type u_1} [MeasurableSpace α] (s : Set α) :
Prop

`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)

Equations

- MeasurableSet s = MeasurableSpace.MeasurableSet' inst✝ s

Instances For

source
def MeasureTheory.«termMeasurableSet[_]» :
Lean.ParserDescr

Notation for `MeasurableSet` with respect to a non-standard σ-algebra.

Equations

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

Instances For

source
@[simp]
theorem MeasurableSet.empty {α : Type u_1} [MeasurableSpace α] :
MeasurableSet ∅
source
theorem MeasurableSet.compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} :
MeasurableSet s → MeasurableSet s ᶜ
source
theorem MeasurableSet.of_compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} (h : MeasurableSet s ᶜ) :
MeasurableSet s
source
@[simp]
theorem MeasurableSet.compl_iff {α : Type u_1} {s : Set α} {m : MeasurableSpace α} :
MeasurableSet s ᶜ ↔ MeasurableSet s
source
@[simp]
theorem MeasurableSet.univ {α : Type u_1} {m : MeasurableSpace α} :
MeasurableSet Set.univ
source
theorem Subsingleton.measurableSet {α : Type u_1} {m : MeasurableSpace α} [Subsingleton α] {s : Set α} :
MeasurableSet s
source
theorem MeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (hs : MeasurableSet s) (h : s = t) :
MeasurableSet t
source
theorem MeasurableSet.iUnion {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] ⦃f : ι → Set α⦄ (h : ∀ (b : ι), MeasurableSet (f b)) :
MeasurableSet (⋃ (b : ι), f b)
source
theorem MeasurableSet.biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋃ b ∈ s, f b)
source
theorem Set.Finite.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : s.Finite) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋃ b ∈ s, f b)
source
theorem Finset.measurableSet_biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋃ b ∈ s, f b)
source
theorem MeasurableSet.sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) :
MeasurableSet (⋃₀ s)
source
theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasurableSet t) :
MeasurableSet (⋃₀ s)
source
theorem MeasurableSet.iInter {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] {f : ι → Set α} (h : ∀ (b : ι), MeasurableSet (f b)) :
MeasurableSet (⋂ (b : ι), f b)
source
theorem MeasurableSet.biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋂ b ∈ s, f b)
source
theorem Set.Finite.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : s.Finite) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋂ b ∈ s, f b)
source
theorem Finset.measurableSet_biInter {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β) (h : ∀ b ∈ s, MeasurableSet (f b)) :
MeasurableSet (⋂ b ∈ s, f b)
source
theorem MeasurableSet.sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) :
MeasurableSet (⋂₀ s)
source
theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasurableSet t) :
MeasurableSet (⋂₀ s)
source
@[simp]
theorem MeasurableSet.union {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (s₁ ∪ s₂)
source
@[simp]
theorem MeasurableSet.inter {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (s₁ ∩ s₂)
source
@[simp]
theorem MeasurableSet.diff {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (s₁ \ s₂)
source
@[simp]
theorem MeasurableSet.himp {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (s₁ ⇨ s₂)
source
@[simp]
theorem MeasurableSet.symmDiff {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (symmDiff s₁ s₂)
source
@[simp]
theorem MeasurableSet.bihimp {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (bihimp s₁ s₂)
source
@[simp]
theorem MeasurableSet.ite {α : Type u_1} {m : MeasurableSpace α} {t s₁ s₂ : Set α} (ht : MeasurableSet t) (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
MeasurableSet (t.ite s₁ s₂)
source
theorem MeasurableSet.ite' {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) :
MeasurableSet (if p then s else t)
source
@[simp]
theorem MeasurableSet.cond {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} :
MeasurableSet (bif i then s₁ else s₂)
source
theorem MeasurableSet.const {α : Type u_1} {m : MeasurableSpace α} (p : Prop) :
MeasurableSet {_a : α | p}
source
theorem nonempty_measurable_superset {α : Type u_1} {m : MeasurableSpace α} (s : Set α) :
Nonempty { t : Set α // s ⊆ t ∧ MeasurableSet t }

Every set has a measurable superset. Declare this as local instance as needed.

source
theorem MeasurableSpace.measurableSet_injective {α : Type u_1} :
Function.Injective (@MeasurableSet α)
source
theorem MeasurableSpace.ext {α : Type u_1} {m₁ m₂ : MeasurableSpace α} (h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s) :
m₁ = m₂
source
theorem MeasurableSpace.ext_iff {α : Type u_1} {m₁ m₂ : MeasurableSpace α} :
m₁ = m₂ ↔ ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
source
class MeasurableSingletonClass (α : Type u_7) [MeasurableSpace α] :
Prop

A typeclass mixin for `MeasurableSpace`s such that each singleton is measurable.

- measurableSet_singleton (x : α) : MeasurableSet {x}

  A singleton is a measurable set.

Instances

source
@[simp]
theorem MeasurableSet.singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
MeasurableSet {a}
source
theorem measurableSet_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} :
MeasurableSet {x : α | x = a}
source
theorem MeasurableSet.insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : α) :
MeasurableSet (insert a s)
source
@[simp]
theorem measurableSet_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} {s : Set α} :
MeasurableSet (insert a s) ↔ MeasurableSet s
source
theorem Set.Subsingleton.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Subsingleton) :
MeasurableSet s
source
theorem Set.Finite.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Finite) :
MeasurableSet s
source
theorem Finset.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) :
MeasurableSet ↑s
source
theorem Set.Countable.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Countable) :
MeasurableSet s
source
def MeasurableSpace.copy {α : Type u_1} (m : MeasurableSpace α) (p : Set α → Prop) (h : ∀ (s : Set α), p s ↔ MeasurableSet s) :
MeasurableSpace α

Copy of a `MeasurableSpace` with a new `MeasurableSet` equal to the old one. Useful to fix definitional equalities.

Equations

- m.copy p h = { MeasurableSet' := p, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

Instances For

source
theorem MeasurableSpace.measurableSet_copy {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s) {s : Set α} :
MeasurableSet s ↔ p s
source
theorem MeasurableSpace.copy_eq {α : Type u_1} {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ (s : Set α), p s ↔ MeasurableSet s) :
m.copy p h = m
source
instance MeasurableSpace.instLE {α : Type u_1} :
LE (MeasurableSpace α)
Equations

- MeasurableSpace.instLE = { le := fun (m₁ m₂ : MeasurableSpace α) => ∀ (s : Set α), MeasurableSet s → MeasurableSet s }

source
theorem MeasurableSpace.le_def {α : Type u_7} {a b : MeasurableSpace α} :
a ≤ b ↔ MeasurableSet' a ≤ MeasurableSet' b
source
instance MeasurableSpace.instPartialOrder {α : Type u_1} :
PartialOrder (MeasurableSpace α)
Equations

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

source
inductive MeasurableSpace.GenerateMeasurable {α : Type u_1} (s : Set (Set α)) :
Set α → Prop

The smallest σ-algebra containing a collection `s` of basic sets

- basic {α : Type u_1} {s : Set (Set α)} (u : Set α) : u ∈ s → GenerateMeasurable s u
- empty {α : Type u_1} {s : Set (Set α)} : GenerateMeasurable s ∅
- compl {α : Type u_1} {s : Set (Set α)} (t : Set α) : GenerateMeasurable s t → GenerateMeasurable s t ᶜ
- iUnion {α : Type u_1} {s : Set (Set α)} (f : ℕ → Set α) : (∀ (n : ℕ), GenerateMeasurable s (f n)) → GenerateMeasurable s (⋃ (i : ℕ), f i)

Instances For

source
def MeasurableSpace.generateFrom {α : Type u_1} (s : Set (Set α)) :
MeasurableSpace α

Construct the smallest measure space containing a collection of basic sets

Equations

- MeasurableSpace.generateFrom s = { MeasurableSet' := MeasurableSpace.GenerateMeasurable s, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

Instances For

source
theorem MeasurableSpace.measurableSet_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) :
MeasurableSet t
source
theorem MeasurableSpace.generateFrom_induction {α : Type u_1} (C : Set (Set α)) (p : (s : Set α) → MeasurableSet s → Prop) (hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht) (empty : p ∅ ⋯) (compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p t ᶜ ⋯) (iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯) (s : Set α) (hs : MeasurableSet s) :
p s hs
source
theorem MeasurableSpace.generateFrom_le {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α} (h : ∀ t ∈ s, MeasurableSet t) :
generateFrom s ≤ m
source
theorem MeasurableSpace.generateFrom_le_iff {α : Type u_1} {s : Set (Set α)} (m : MeasurableSpace α) :
generateFrom s ≤ m ↔ s ⊆ {t : Set α | MeasurableSet t}
source
@[simp]
theorem MeasurableSpace.generateFrom_measurableSet {α : Type u_1} [MeasurableSpace α] :
generateFrom {s : Set α | MeasurableSet s} = inst✝
source
theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff {α : Type u_1} {S : Set (Set α)} {x y : α} :
(∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s
source
def MeasurableSpace.mkOfClosure {α : Type u_1} (g : Set (Set α)) (hg : {t : Set α | MeasurableSet t} = g) :
MeasurableSpace α

If `g` is a collection of subsets of `α` such that the `σ`-algebra generated from `g` contains the same sets as `g`, then `g` was already a `σ`-algebra.

Equations

- MeasurableSpace.mkOfClosure g hg = (MeasurableSpace.generateFrom g).copy (fun (x : Set α) => x ∈ g) ⋯

Instances For

source
theorem MeasurableSpace.mkOfClosure_sets {α : Type u_1} {s : Set (Set α)} {hs : {t : Set α | MeasurableSet t} = s} :
MeasurableSpace.mkOfClosure s hs = generateFrom s
source
def MeasurableSpace.giGenerateFrom {α : Type u_1} :
GaloisInsertion generateFrom fun (m : MeasurableSpace α) => {t : Set α | MeasurableSet t}

We get a Galois insertion between `σ`-algebras on `α` and `Set (Set α)` by using `generate_from` on one side and the collection of measurable sets on the other side.

Equations

- MeasurableSpace.giGenerateFrom = { choice := fun (g : Set (Set α)) (hg : {t : Set α | MeasurableSet t} ≤ g) => MeasurableSpace.mkOfClosure g ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source
instance MeasurableSpace.instCompleteLattice {α : Type u_1} :
CompleteLattice (MeasurableSpace α)
Equations

- MeasurableSpace.instCompleteLattice = MeasurableSpace.giGenerateFrom.liftCompleteLattice

source
instance MeasurableSpace.instInhabited {α : Type u_1} :
Inhabited (MeasurableSpace α)
Equations

- MeasurableSpace.instInhabited = { default := ⊤ }

source
theorem MeasurableSpace.generateFrom_mono {α : Type u_1} {s t : Set (Set α)} (h : s ⊆ t) :
generateFrom s ≤ generateFrom t
source
theorem MeasurableSpace.generateFrom_sup_generateFrom {α : Type u_1} {s t : Set (Set α)} :
generateFrom s ⊔ generateFrom t = generateFrom (s ∪ t)
source
theorem MeasurableSpace.iSup_generateFrom {α : Type u_1} {ι : Sort u_6} (s : ι → Set (Set α)) :
⨆ (i : ι), generateFrom (s i) = generateFrom (⋃ (i : ι), s i)
source
@[simp]
theorem MeasurableSpace.generateFrom_empty {α : Type u_1} :
generateFrom ∅ = ⊥
source
theorem MeasurableSpace.generateFrom_singleton_empty {α : Type u_1} :
generateFrom {∅} = ⊥
source
theorem MeasurableSpace.generateFrom_singleton_univ {α : Type u_1} :
generateFrom {Set.univ} = ⊥
source
@[simp]
theorem MeasurableSpace.generateFrom_insert_univ {α : Type u_1} (S : Set (Set α)) :
generateFrom (insert Set.univ S) = generateFrom S
source
@[simp]
theorem MeasurableSpace.generateFrom_insert_empty {α : Type u_1} (S : Set (Set α)) :
generateFrom (insert ∅ S) = generateFrom S
source
theorem MeasurableSpace.measurableSet_bot_iff {α : Type u_1} {s : Set α} :
MeasurableSet s ↔ s = ∅ ∨ s = Set.univ
source
@[simp]
theorem MeasurableSpace.measurableSet_top {α : Type u_1} {s : Set α} :
MeasurableSet s
source
@[simp]
theorem MeasurableSpace.measurableSet_inf {α : Type u_1} {m₂ m₁ : MeasurableSpace α} {s : Set α} :
MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
source
@[simp]
theorem MeasurableSpace.measurableSet_sInf {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} :
MeasurableSet s ↔ ∀ m ∈ ms, MeasurableSet s
source
theorem MeasurableSpace.measurableSet_iInf {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} :
MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
source
theorem MeasurableSpace.measurableSet_sup {α : Type u_1} {m₁ m₂ : MeasurableSpace α} {s : Set α} :
MeasurableSet s ↔ GenerateMeasurable (MeasurableSet ∪ MeasurableSet) s
source
theorem MeasurableSpace.measurableSet_sSup {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} :
MeasurableSet s ↔ GenerateMeasurable {s : Set α | ∃ m ∈ ms, MeasurableSet s} s
source
theorem MeasurableSpace.measurableSet_iSup {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} :
MeasurableSet s ↔ GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s
source
theorem MeasurableSpace.measurableSpace_iSup_eq {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) :
⨆ (n : ι), m n = generateFrom {s : Set α | ∃ (n : ι), MeasurableSet s}
source
theorem MeasurableSpace.generateFrom_iUnion_measurableSet {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) :
generateFrom (⋃ (n : ι), {t : Set α | MeasurableSet t}) = ⨆ (n : ι), m n
source
def Measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) :
Prop

A function `f` between measurable spaces is measurable if the preimage of every measurable set is measurable.

Equations

- Measurable f = ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)

Instances For

source
def MeasureTheory.«termMeasurable[_]» :
Lean.ParserDescr

Notation for `Measurable` with respect to a non-standard σ-algebra in the domain.

Equations

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

Instances For

source
def MeasureTheory.«termMeasurable[_,_]» :
Lean.ParserDescr

Notation for `Measurable` with respect to a non-standard σ-algebra in the domain and codomain.

Equations

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

Instances For

source
theorem measurable_id {α : Type u_1} {x✝ : MeasurableSpace α} :
Measurable id
source
theorem measurable_id' {α : Type u_1} {x✝ : MeasurableSpace α} :
Measurable fun (a : α) => a
source
theorem Measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace γ} {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) :
Measurable (g ∘ f)
source
theorem Measurable.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {x✝² : MeasurableSpace γ} {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) :
Measurable fun (x : α) => g (f x)
source
@[simp]
theorem measurable_const {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {a : α} :
Measurable fun (x : β) => a
source
theorem Measurable.le {β : Type u_2} {α : Type u_7} {m m0 : MeasurableSpace α} {x✝ : MeasurableSpace β} (hm : m ≤ m0) {f : α → β} (hf : Measurable f) :
Measurable f
source
class DiscreteMeasurableSpace (α : Type u_7) [MeasurableSpace α] :
Prop

A typeclass mixin for `MeasurableSpace`s such that all sets are measurable.

- forall_measurableSet (s : Set α) : MeasurableSet s

  Do not use this. Use `MeasurableSet.of_discrete` instead.

Instances

source
instance instDiscreteMeasurableSpace {α : Type u_1} :
DiscreteMeasurableSpace α
source
@[instance 100]
instance MeasurableSingletonClass.toDiscreteMeasurableSpace {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] :
DiscreteMeasurableSpace α
source
theorem MeasurableSet.of_discrete {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] {s : Set α} :
MeasurableSet s
source
theorem Measurable.of_discrete {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace α] {f : α → β} :
Measurable f
source
@[instance 100]
instance DiscreteMeasurableSpace.toMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] :
MeasurableSingletonClass α

Warning: Creates a typeclass loop with `MeasurableSingletonClass.toDiscreteMeasurableSpace`. To be monitored.