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

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 : self.MeasurableSet' ∅

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

• measurableSet_compl : ∀ (s : Set α), self.MeasurableSet' s → self.MeasurableSet' sᶜ

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

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

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

theorem MeasurableSpace.measurableSet_empty {α : Type u_7} (self : MeasurableSpace α) : self.MeasurableSet' ∅

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

theorem MeasurableSpace.measurableSet_compl {α : Type u_7} (self : MeasurableSpace α) (s : Set α) : self.MeasurableSet' s → self.MeasurableSet' sᶜ

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

theorem MeasurableSpace.measurableSet_iUnion {α : Type u_7} (self : MeasurableSpace α) (f : ℕ → Set α) : (∀ (i : ℕ), self.MeasurableSet' (f i)) → self.MeasurableSet' (⋃ (i : ℕ), f i)

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

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

Equations

• instMeasurableSpaceOrderDual = h

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 = inst.MeasurableSet' s

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.

@[simp]

theorem MeasurableSet.empty {α : Type u_1} [MeasurableSpace α] : MeasurableSet ∅

theorem MeasurableSet.compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} : MeasurableSet s → MeasurableSet sᶜ

theorem MeasurableSet.of_compl {α : Type u_1} {s : Set α} {m : MeasurableSpace α} (h : MeasurableSet sᶜ) : MeasurableSet s

@[simp]

theorem MeasurableSet.compl_iff {α : Type u_1} {s : Set α} {m : MeasurableSpace α} : MeasurableSet sᶜ ↔ MeasurableSet s

@[simp]

theorem MeasurableSet.univ {α : Type u_1} {m : MeasurableSpace α} : MeasurableSet Set.univ

theorem Subsingleton.measurableSet {α : Type u_1} {m : MeasurableSpace α} [Subsingleton α] {s : Set α} : MeasurableSet s

theorem MeasurableSet.congr {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (hs : MeasurableSet s) (h : s = t) : MeasurableSet t

theorem MeasurableSet.iUnion {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] ⦃f : ι → Set α⦄ (h : ∀ (b : ι), MeasurableSet (f b)) : MeasurableSet (⋃ (b : ι), f b)

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)

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)

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)

theorem MeasurableSet.sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋃₀ s)

theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋃₀ s)

theorem MeasurableSet.iInter {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] {f : ι → Set α} (h : ∀ (b : ι), MeasurableSet (f b)) : MeasurableSet (⋂ (b : ι), f b)

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)

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)

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)

theorem MeasurableSet.sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋂₀ s)

theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋂₀ s)

@[simp]

theorem MeasurableSet.union {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∪ s₂)

@[simp]

theorem MeasurableSet.inter {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∩ s₂)

@[simp]

theorem MeasurableSet.diff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ \ s₂)

@[simp]

theorem MeasurableSet.himp {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ⇨ s₂)

@[simp]

theorem MeasurableSet.symmDiff {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (symmDiff s₁ s₂)

@[simp]

theorem MeasurableSet.bihimp {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (bihimp s₁ s₂)

@[simp]

theorem MeasurableSet.ite {α : Type u_1} {m : MeasurableSpace α} {t : Set α} {s₁ : Set α} {s₂ : Set α} (ht : MeasurableSet t) (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (t.ite s₁ s₂)

theorem MeasurableSet.ite' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) : MeasurableSet (if p then s else t)

@[simp]

theorem MeasurableSet.cond {α : Type u_1} {m : MeasurableSpace α} {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} : MeasurableSet (bif i then s₁ else s₂)

@[simp]

theorem MeasurableSet.disjointed {α : Type u_1} {m : MeasurableSpace α} {f : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (f i)) (n : ℕ) : MeasurableSet (disjointed f n)

theorem MeasurableSet.const {α : Type u_1} {m : MeasurableSpace α} (p : Prop) : MeasurableSet {_a : α | p}

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.

theorem MeasurableSpace.measurableSet_injective {α : Type u_1} : Function.Injective (@MeasurableSet α)

theorem MeasurableSpace.ext {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} (h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s) : m₁ = m₂

class MeasurableSingletonClass (α : Type u_7) [MeasurableSpace α] : Prop

A typeclass mixin for MeasurableSpaces such that each singleton is measurable.

• measurableSet_singleton : ∀ (x : α), MeasurableSet {x}

  A singleton is a measurable set.

theorem MeasurableSingletonClass.measurableSet_singleton {α : Type u_7} : ∀ {inst : MeasurableSpace α} [self : MeasurableSingletonClass α] (x : α), MeasurableSet {x}

A singleton is a measurable set.

@[simp]

theorem MeasurableSet.singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : MeasurableSet {a}

theorem measurableSet_eq {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} : MeasurableSet {x : α | x = a}

theorem MeasurableSet.insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : MeasurableSet s) (a : α) : MeasurableSet (insert a s)

@[simp]

theorem measurableSet_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {a : α} {s : Set α} : MeasurableSet (insert a s) ↔ MeasurableSet s

theorem Set.Subsingleton.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Subsingleton) : MeasurableSet s

theorem Set.Finite.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Finite) : MeasurableSet s

theorem Finset.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) : MeasurableSet ↑s

theorem Set.Countable.measurableSet {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α} (hs : s.Countable) : MeasurableSet s

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 := ⋯ }

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

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

instance MeasurableSpace.instLE {α : Type u_1} : LE (MeasurableSpace α)

Equations

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

theorem MeasurableSpace.le_def {α : Type u_7} {a : MeasurableSpace α} {b : MeasurableSpace α} : a ≤ b ↔ a.MeasurableSet' ≤ b.MeasurableSet'

instance MeasurableSpace.instPartialOrder {α : Type u_1} : PartialOrder (MeasurableSpace α)

Equations

• MeasurableSpace.instPartialOrder = PartialOrder.mk ⋯

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 ∈ s, MeasurableSpace.GenerateMeasurable s u
• empty: ∀ {α : Type u_1} {s : Set (Set α)}, MeasurableSpace.GenerateMeasurable s ∅
• compl: ∀ {α : Type u_1} {s : Set (Set α)} (t : Set α), MeasurableSpace.GenerateMeasurable s t → MeasurableSpace.GenerateMeasurable s tᶜ
• iUnion: ∀ {α : Type u_1} {s : Set (Set α)} (f : ℕ → Set α), (∀ (n : ℕ), MeasurableSpace.GenerateMeasurable s (f n)) → MeasurableSpace.GenerateMeasurable s (⋃ (i : ℕ), f i)

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 := ⋯ }

theorem MeasurableSpace.measurableSet_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) : MeasurableSet t

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

theorem MeasurableSpace.generateFrom_le {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α} (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSpace.generateFrom s ≤ m

theorem MeasurableSpace.generateFrom_le_iff {α : Type u_1} {s : Set (Set α)} (m : MeasurableSpace α) : MeasurableSpace.generateFrom s ≤ m ↔ s ⊆ {t : Set α | MeasurableSet t}

@[simp]

theorem MeasurableSpace.generateFrom_measurableSet {α : Type u_1} [MeasurableSpace α] : MeasurableSpace.generateFrom {s : Set α | MeasurableSet s} = inst✝

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

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) ⋯

theorem MeasurableSpace.mkOfClosure_sets {α : Type u_1} {s : Set (Set α)} {hs : {t : Set α | MeasurableSet t} = s} : MeasurableSpace.mkOfClosure s hs = MeasurableSpace.generateFrom s

def MeasurableSpace.giGenerateFrom {α : Type u_1} : GaloisInsertion MeasurableSpace.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 := ⋯ }

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

Equations

• MeasurableSpace.instCompleteLattice = MeasurableSpace.giGenerateFrom.liftCompleteLattice

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

Equations

• MeasurableSpace.instInhabited = { default := ⊤ }

theorem MeasurableSpace.generateFrom_mono {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} (h : s ⊆ t) : MeasurableSpace.generateFrom s ≤ MeasurableSpace.generateFrom t

theorem MeasurableSpace.generateFrom_sup_generateFrom {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} : MeasurableSpace.generateFrom s ⊔ MeasurableSpace.generateFrom t = MeasurableSpace.generateFrom (s ∪ t)

theorem MeasurableSpace.iSup_generateFrom {α : Type u_1} {ι : Sort u_6} (s : ι → Set (Set α)) : ⨆ (i : ι), MeasurableSpace.generateFrom (s i) = MeasurableSpace.generateFrom (⋃ (i : ι), s i)

@[simp]

theorem MeasurableSpace.generateFrom_empty {α : Type u_1} : MeasurableSpace.generateFrom ∅ = ⊥

theorem MeasurableSpace.generateFrom_singleton_empty {α : Type u_1} : MeasurableSpace.generateFrom {∅} = ⊥

theorem MeasurableSpace.generateFrom_singleton_univ {α : Type u_1} : MeasurableSpace.generateFrom {Set.univ} = ⊥

@[simp]

theorem MeasurableSpace.generateFrom_insert_univ {α : Type u_1} (S : Set (Set α)) : MeasurableSpace.generateFrom (insert Set.univ S) = MeasurableSpace.generateFrom S

@[simp]

theorem MeasurableSpace.generateFrom_insert_empty {α : Type u_1} (S : Set (Set α)) : MeasurableSpace.generateFrom (insert ∅ S) = MeasurableSpace.generateFrom S

theorem MeasurableSpace.measurableSet_bot_iff {α : Type u_1} {s : Set α} : MeasurableSet s ↔ s = ∅ ∨ s = Set.univ

@[simp]

theorem MeasurableSpace.measurableSet_top {α : Type u_1} {s : Set α} : MeasurableSet s

@[simp]

theorem MeasurableSpace.measurableSet_inf {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

@[simp]

theorem MeasurableSpace.measurableSet_sInf {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} : MeasurableSet s ↔ ∀ m ∈ ms, MeasurableSet s

theorem MeasurableSpace.measurableSet_iInf {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s

theorem MeasurableSpace.measurableSet_sup {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable (MeasurableSet ∪ MeasurableSet) s

theorem MeasurableSpace.measurableSet_sSup {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s : Set α | ∃ m ∈ ms, MeasurableSet s} s

theorem MeasurableSpace.measurableSet_iSup {α : Type u_1} {ι : Sort u_7} {m : ι → MeasurableSpace α} {s : Set α} : MeasurableSet s ↔ MeasurableSpace.GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s

theorem MeasurableSpace.measurableSpace_iSup_eq {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) : ⨆ (n : ι), m n = MeasurableSpace.generateFrom {s : Set α | ∃ (n : ι), MeasurableSet s}

theorem MeasurableSpace.generateFrom_iUnion_measurableSet {α : Type u_1} {ι : Sort u_6} (m : ι → MeasurableSpace α) : MeasurableSpace.generateFrom (⋃ (n : ι), {t : Set α | MeasurableSet t}) = ⨆ (n : ι), m n

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)

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.

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.

theorem measurable_id {α : Type u_1} : ∀ {x : MeasurableSpace α}, Measurable id

theorem measurable_id' {α : Type u_1} : ∀ {x : MeasurableSpace α}, Measurable fun (a : α) => a

theorem Measurable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable (g ∘ f)

theorem Measurable.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable fun (x : α) => g (f x)

@[simp]

theorem measurable_const {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun (x : β) => a

theorem Measurable.le {β : Type u_2} {α : Type u_7} {m : MeasurableSpace α} {m0 : MeasurableSpace α} : ∀ {x : MeasurableSpace β}, m ≤ m0 → ∀ {f : α → β}, Measurable f → Measurable f

class DiscreteMeasurableSpace (α : Type u_7) [MeasurableSpace α] : Prop

A typeclass mixin for MeasurableSpaces such that all sets are measurable.

• forall_measurableSet : ∀ (s : Set α), MeasurableSet s

  Do not use this. Use MeasurableSet.of_discrete instead.

theorem DiscreteMeasurableSpace.forall_measurableSet {α : Type u_7} : ∀ {inst : MeasurableSpace α} [self : DiscreteMeasurableSpace α] (s : Set α), MeasurableSet s

Do not use this. Use MeasurableSet.of_discrete instead.

instance instDiscreteMeasurableSpace {α : Type u_1} : DiscreteMeasurableSpace α

Equations

• ⋯ = ⋯

@[instance 100]

instance MeasurableSingletonClass.toDiscreteMeasurableSpace {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] : DiscreteMeasurableSpace α

Equations

• ⋯ = ⋯

theorem MeasurableSet.of_discrete {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] {s : Set α} : MeasurableSet s

theorem Measurable.of_discrete {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace α] {f : α → β} : Measurable f

@[deprecated MeasurableSet.of_discrete]

theorem measurableSet_discrete {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] (s : Set α) : MeasurableSet s

@[deprecated Measurable.of_discrete]

theorem measurable_discrete {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace α] (f : α → β) : Measurable f

@[instance 100]

instance DiscreteMeasurableSpace.toMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] : MeasurableSingletonClass α

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

Equations

• ⋯ = ⋯