Documentation

Mathlib.MeasureTheory.MeasurableSpace.Defs

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 #

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.

Instances

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

MeasurableSpace αᵒᵈ

Equations

instMeasurableSpaceOrderDual = h

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

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

Equations

MeasurableSet s = inst.MeasurableSet' s

Instances For

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)

@[deprecated MeasurableSet.iUnion]

theorem MeasurableSet.biUnion_decode₂ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Encodable β] ⦃f : β → Set α⦄ (h : ∀ (b : β), MeasurableSet (f b)) (n : ℕ) :

MeasurableSet (⋃ b ∈ Encodable.decode₂ β n, f b)

theorem MeasurableSet.biUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β} (hs : Set.Countable s) (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 : Set.Finite s) (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 : Set.Countable s) (h : ∀ t ∈ s, MeasurableSet t) :

MeasurableSet (⋃₀ s)

theorem Set.Finite.measurableSet_sUnion {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Finite s) (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 : Set.Countable s) (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 : Set.Finite s) (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 : Set.Countable s) (h : ∀ t ∈ s, MeasurableSet t) :

MeasurableSet (⋂₀ s)

theorem Set.Finite.measurableSet_sInter {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)} (hs : Set.Finite s) (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 (Set.ite t 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₂

theorem MeasurableSpace.ext_iff {α : Type u_1} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} :

m₁ = m₂ ↔ ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s

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

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

measurableSet_singleton : ∀ (x : α), MeasurableSet {x}
A singleton is a measurable set.

Instances

@[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 : Set.Subsingleton s) :

MeasurableSet s

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

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 : Set.Countable s) :

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

MeasurableSpace.copy m 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) :

MeasurableSpace.copy m p h = m

instance MeasurableSpace.instLEMeasurableSpace {α : Type u_1} :

LE (MeasurableSpace α)

Equations

MeasurableSpace.instLEMeasurableSpace = { 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.instPartialOrderMeasurableSpace {α : Type u_1} :

PartialOrder (MeasurableSpace α)

Equations

MeasurableSpace.instPartialOrderMeasurableSpace = let __src := PartialOrder.lift (@MeasurableSet α) ⋯; 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} (p : Set α → Prop) (C : Set (Set α)) (hC : ∀ t ∈ C, p t) (h_empty : p ∅) (h_compl : ∀ (t : Set α), p t → p tᶜ) (h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)) {s : Set α} (hs : MeasurableSet s) :

p s

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.copy (MeasurableSpace.generateFrom g) (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.instCompleteLatticeMeasurableSpace {α : Type u_1} :

CompleteLattice (MeasurableSpace α)

Equations

MeasurableSpace.instCompleteLatticeMeasurableSpace = GaloisInsertion.liftCompleteLattice MeasurableSpace.giGenerateFrom

instance MeasurableSpace.instInhabitedMeasurableSpace {α : Type u_1} :

Inhabited (MeasurableSpace α)

Equations

MeasurableSpace.instInhabitedMeasurableSpace = { 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 : α → β) :

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-standanrd σ-algebra in the domain.

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 α] :

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

forall_measurableSet : ∀ (s : Set α), MeasurableSet s
Do not use this. Use measurableSet_discrete instead.

Instances

instance instDiscreteMeasurableSpaceTopMeasurableSpaceToTopInstCompleteLatticeMeasurableSpace {α : Type u_1} :

DiscreteMeasurableSpace α

Equations

⋯ = ⋯

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

DiscreteMeasurableSpace α

Equations

⋯ = ⋯

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

MeasurableSet s

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

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

MeasurableSingletonClass α

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

Equations

⋯ = ⋯