# Measurable spaces and measurable functions #

This file provides properties of measurable spaces and the functions and isomorphisms between them. The definition of a measurable space is in Mathlib/MeasureTheory/MeasurableSpace/Defs.lean.

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. A function f : α → β induces a Galois connection between the lattices of σ-algebras on α and β.

A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.

We say that a filter f is measurably generated if every set s ∈ f includes a measurable set t ∈ f. This property is useful, e.g., to extract a measurable witness of Filter.Eventually.

## Notation #

• We write α ≃ᵐ β for measurable equivalences between the measurable spaces α and β. This should not be confused with ≃ₘ which is used for diffeomorphisms between manifolds.

## Implementation notes #

Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.

## Tags #

measurable space, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system

def MeasurableSpace.map {α : Type u_1} {β : Type u_2} (f : αβ) (m : ) :

The forward image of a measurable space under a function. map f m contains the sets s : Set β whose preimage under f is measurable.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableSpace.map_def {α : Type u_1} {β : Type u_2} {m : } {f : αβ} {s : Set β} :
@[simp]
theorem MeasurableSpace.map_id {α : Type u_1} {m : } :
= m
@[simp]
theorem MeasurableSpace.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {f : αβ} {g : βγ} :
def MeasurableSpace.comap {α : Type u_1} {β : Type u_2} (f : αβ) (m : ) :

The reverse image of a measurable space under a function. comap f m contains the sets s : Set α such that s is the f-preimage of a measurable set in β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableSpace.comap_eq_generateFrom {α : Type u_1} {β : Type u_2} (m : ) (f : αβ) :
= MeasurableSpace.generateFrom {t : Set α | ∃ (s : Set β), f ⁻¹' s = t}
@[simp]
theorem MeasurableSpace.comap_id {α : Type u_1} {m : } :
= m
@[simp]
theorem MeasurableSpace.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {f : βα} {g : γβ} :
theorem MeasurableSpace.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : } {m' : } {f : αβ} :
m m'
theorem MeasurableSpace.gc_comap_map {α : Type u_1} {β : Type u_2} (f : αβ) :
theorem MeasurableSpace.map_mono {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} (h : m₁ m₂) :
theorem MeasurableSpace.monotone_map {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem MeasurableSpace.comap_mono {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {g : βα} (h : m₁ m₂) :
theorem MeasurableSpace.monotone_comap {α : Type u_1} {β : Type u_2} {g : βα} :
@[simp]
theorem MeasurableSpace.comap_bot {α : Type u_1} {β : Type u_2} {g : βα} :
@[simp]
theorem MeasurableSpace.comap_sup {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {g : βα} :
MeasurableSpace.comap g (m₁ m₂) =
@[simp]
theorem MeasurableSpace.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : βα} {m : ι} :
MeasurableSpace.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), MeasurableSpace.comap g (m i)
@[simp]
theorem MeasurableSpace.map_top {α : Type u_1} {β : Type u_2} {f : αβ} :
@[simp]
theorem MeasurableSpace.map_inf {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
MeasurableSpace.map f (m₁ m₂) =
@[simp]
theorem MeasurableSpace.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : αβ} {m : ι} :
MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)
theorem MeasurableSpace.comap_map_le {α : Type u_1} {β : Type u_2} {m : } {f : αβ} :
theorem MeasurableSpace.le_map_comap {α : Type u_1} {β : Type u_2} {m : } {g : βα} :
@[simp]
theorem MeasurableSpace.map_const {α : Type u_1} {β : Type u_2} {m : } (b : β) :
MeasurableSpace.map (fun (_a : α) => b) m =
@[simp]
theorem MeasurableSpace.comap_const {α : Type u_1} {β : Type u_2} {m : } (b : β) :
MeasurableSpace.comap (fun (_a : α) => b) m =
theorem MeasurableSpace.comap_generateFrom {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set (Set β)} :
theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₂
theorem Measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₂

Alias of the forward direction of measurable_iff_le_map.

theorem Measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₂

Alias of the reverse direction of measurable_iff_le_map.

theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₁
theorem Measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₁

Alias of the reverse direction of measurable_iff_comap_le.

theorem Measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : } {m₂ : } {f : αβ} :
m₁

Alias of the forward direction of measurable_iff_comap_le.

theorem comap_measurable {α : Type u_1} {β : Type u_2} {m : } (f : αβ) :
theorem Measurable.mono {α : Type u_1} {β : Type u_2} {ma : } {ma' : } {mb : } {mb' : } {f : αβ} (hf : ) (ha : ma ma') (hb : mb' mb) :
theorem measurable_id'' {α : Type u_1} {m : } {mα : } (hm : m ) :
theorem measurable_from_top {α : Type u_1} {β : Type u_2} [] {f : αβ} :
theorem measurable_generateFrom {α : Type u_1} {β : Type u_2} [] {s : Set (Set β)} {f : αβ} (h : ts, MeasurableSet (f ⁻¹' t)) :
theorem Subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : αβ} [] [] [] :
theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) :
theorem measurable_zero {α : Type u_1} {β : Type u_2} [] [] [Zero α] :
theorem measurable_one {α : Type u_1} {β : Type u_2} [] [] [One α] :
theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) :
theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) :
theorem measurable_const' {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ∀ (x y : β), f x = f y) :

A version of measurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

theorem measurable_natCast {α : Type u_1} {β : Type u_2} [] [] [] (n : ) :
theorem measurable_intCast {α : Type u_1} {β : Type u_2} [] [] [] (n : ) :
theorem measurable_of_countable {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) :
theorem measurable_of_finite {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) :
theorem Measurable.iterate {α : Type u_1} {m : } {f : αα} (hf : ) (n : ) :
theorem measurableSet_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : } {mβ : } {t : Set β} (hf : ) (ht : ) :
theorem MeasurableSet.preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : } {mβ : } {t : Set β} (ht : ) (hf : ) :
theorem Measurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {g : αβ} {m : } {mβ : } :
∀ {x : DecidablePred fun (x : α) => x s}, Measurable ()
theorem Measurable.ite {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : } {mβ : } {p : αProp} :
∀ {x : }, MeasurableSet {a : α | p a}Measurable fun (x_1 : α) => if p x_1 then f x_1 else g x_1

This is slightly different from Measurable.piecewise. It can be used to show Measurable (ite (x=0) 0 1) by exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const, but replacing Measurable.ite by Measurable.piecewise in that example proof does not work.

theorem Measurable.indicator {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {m : } {mβ : } [Zero β] (hf : ) (hs : ) :
theorem measurable_indicator_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {m : } {mβ : } [Zero β] (b : β) [] :
Measurable (Set.indicator s fun (x : α) => b)

The measurability of a set A is equivalent to the measurability of the indicator function which takes a constant value b ≠ 0 on a set A and 0 elsewhere.

theorem measurableSet_support {α : Type u_1} {β : Type u_2} {f : αβ} {m : } {mβ : } [Zero β] (hf : ) :
theorem measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : αβ} {m : } {mβ : } [One β] (hf : ) :
theorem Measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : } {mβ : } (hf : ) (h : Set.Countable {x : α | f x g x}) :

If a function coincides with a measurable function outside of a countable set, it is measurable.

Equations
Equations
Equations
Equations
Equations
instance Fin.instMeasurableSpace (n : ) :
Equations
Equations
Equations
instance Subsingleton.measurableSingletonClass {α : Type u_6} [] [] :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} (h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})) :
theorem measurable_to_countable' {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} (h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})) :
theorem measurable_unit {α : Type u_1} [] (f : Unitα) :
Equations
theorem measurable_down {α : Type u_1} [] :
Measurable ULift.down
theorem measurable_up {α : Type u_1} [] :
Measurable ULift.up
@[simp]
theorem measurableSet_preimage_down {α : Type u_1} [] {s : Set α} :
MeasurableSet (ULift.down ⁻¹' s)
@[simp]
theorem measurableSet_preimage_up {α : Type u_1} [] {s : Set ()} :
MeasurableSet (ULift.up ⁻¹' s)
theorem measurable_from_nat {α : Type u_1} [] {f : α} :
theorem measurable_to_nat {α : Type u_1} [] {f : α} :
(∀ (y : α), MeasurableSet (f ⁻¹' {f y}))
theorem measurable_to_bool {α : Type u_1} [] {f : αBool} (h : MeasurableSet (f ⁻¹' {true})) :
theorem measurable_to_prop {α : Type u_1} [] {f : αProp} (h : MeasurableSet (f ⁻¹' {True})) :
theorem measurable_findGreatest' {α : Type u_1} [] {p : α} [(x : α) → DecidablePred (p x)] {N : } (hN : kN, MeasurableSet {x : α | Nat.findGreatest (p x) N = k}) :
Measurable fun (x : α) => Nat.findGreatest (p x) N
theorem measurable_findGreatest {α : Type u_1} [] {p : α} [(x : α) → DecidablePred (p x)] {N : } (hN : kN, MeasurableSet {x : α | p x k}) :
Measurable fun (x : α) => Nat.findGreatest (p x) N
theorem measurable_find {α : Type u_1} [] {p : α} [(x : α) → DecidablePred (p x)] (hp : ∀ (x : α), ∃ (N : ), p x N) (hm : ∀ (k : ), MeasurableSet {x : α | p x k}) :
Measurable fun (x : α) => Nat.find (_ : ∃ (N : ), p x N)
instance Quot.instMeasurableSpace {α : Type u_6} {r : ααProp} [m : ] :
Equations
• Quot.instMeasurableSpace =
instance Quotient.instMeasurableSpace {α : Type u_6} {s : } [m : ] :
Equations
instance QuotientAddGroup.measurableSpace {G : Type u_6} [] [] (S : ) :
Equations
• = Quotient.instMeasurableSpace
instance QuotientGroup.measurableSpace {G : Type u_6} [] [] (S : ) :
Equations
• = Quotient.instMeasurableSpace
theorem measurableSet_quotient {α : Type u_1} [] {s : } {t : Set ()} :
MeasurableSet (Quotient.mk'' ⁻¹' t)
theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} [] [] {s : } {f : β} :
Measurable (f Quotient.mk'')
theorem measurable_quotient_mk' {α : Type u_1} [] [s : ] :
Measurable Quotient.mk'
theorem measurable_quotient_mk'' {α : Type u_1} [] {s : } :
Measurable Quotient.mk''
theorem measurable_quot_mk {α : Type u_1} [] {r : ααProp} :
theorem QuotientAddGroup.measurable_coe {G : Type u_6} [] [] {S : } :
theorem QuotientGroup.measurable_coe {G : Type u_6} [] [] {S : } :
Measurable QuotientGroup.mk
theorem QuotientAddGroup.measurable_from_quotient {α : Type u_1} [] {G : Type u_6} [] [] {S : } {f : G Sα} :
theorem QuotientGroup.measurable_from_quotient {α : Type u_1} [] {G : Type u_6} [] [] {S : } {f : G Sα} :
Measurable (f QuotientGroup.mk)
instance Subtype.instMeasurableSpace {α : Type u_6} {p : αProp} [m : ] :
Equations
theorem measurable_subtype_coe {α : Type u_1} [] {p : αProp} :
Measurable Subtype.val
instance Subtype.instMeasurableSingletonClass {α : Type u_1} [] {p : αProp} :
Equations
• (_ : ) = (_ : )
theorem MeasurableSet.of_subtype_image {α : Type u_1} {m : } {s : Set α} {t : Set s} (h : MeasurableSet (Subtype.val '' t)) :
theorem MeasurableSet.subtype_image {α : Type u_1} {m : } {s : Set α} {t : Set s} (hs : ) :
MeasurableSet (Subtype.val '' t)
theorem Measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : } {mβ : } {p : βProp} {f : α} (hf : ) :
Measurable fun (a : α) => (f a)
theorem Measurable.subtype_val {α : Type u_1} {β : Type u_2} {m : } {mβ : } {p : βProp} {f : α} (hf : ) :
Measurable fun (a : α) => (f a)

Alias of Measurable.subtype_coe.

theorem Measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : } {mβ : } {p : βProp} {f : αβ} (hf : ) {h : ∀ (x : α), p (f x)} :
Measurable fun (x : α) => { val := f x, property := (_ : p (f x)) }
theorem Measurable.rangeFactorization {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (hf : ) :
theorem Measurable.subtype_map {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} {p : αProp} {q : βProp} (hf : ) (hpq : ∀ (x : α), p xq (f x)) :
theorem measurable_inclusion {α : Type u_1} {m : } {s : Set α} {t : Set α} (h : s t) :
theorem MeasurableSet.image_inclusion' {α : Type u_1} {m : } {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : ) :
theorem MeasurableSet.image_inclusion {α : Type u_1} {m : } {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : ) (hu : ) :
theorem MeasurableSet.of_union_cover {α : Type u_1} {m : } {s : Set α} {t : Set α} {u : Set α} (hs : ) (ht : ) (h : Set.univ s t) (hsu : MeasurableSet (Subtype.val ⁻¹' u)) (htu : MeasurableSet (Subtype.val ⁻¹' u)) :
theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (s : Set α) (t : Set α) (hs : ) (ht : ) (h : Set.univ s t) (hc : Measurable fun (a : s) => f a) (hd : Measurable fun (a : t) => f a) :
theorem measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} {s : Set α} (hs : ) (h₁ : Measurable ()) (h₂ : Measurable ()) :
theorem Measurable.dite {α : Type u_1} {β : Type u_2} {s : Set α} {m : } {mβ : } [(x : α) → Decidable (x s)] {f : sβ} (hf : ) {g : sβ} (hg : ) (hs : ) :
Measurable fun (x : α) => if hx : x s then f { val := x, property := hx } else g { val := x, property := hx }
theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (s : Set α) (hs : ) (hf : Measurable ()) :
theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} {m : } {mβ : } {f : αβ} (a : α) (hf : Measurable (Set.restrict {x : α | x a} f)) :
def MeasurableSpace.prod {α : Type u_6} {β : Type u_7} (m₁ : ) (m₂ : ) :

A MeasurableSpace structure on the product of two measurable spaces.

Equations
Instances For
instance Prod.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : ] [m₂ : ] :
Equations
• Prod.instMeasurableSpace =
theorem measurable_fst {α : Type u_1} {β : Type u_2} :
∀ {x : } {x_1 : }, Measurable Prod.fst
theorem measurable_snd {α : Type u_1} {β : Type u_2} :
∀ {x : } {x_1 : }, Measurable Prod.snd
theorem Measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβ × γ} (hf : ) :
Measurable fun (a : α) => (f a).1
theorem Measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβ × γ} (hf : ) :
Measurable fun (a : α) => (f a).2
theorem Measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβ × γ} (hf₁ : Measurable fun (a : α) => (f a).1) (hf₂ : Measurable fun (a : α) => (f a).2) :
theorem Measurable.prod_mk {α : Type u_1} {m : } {β : Type u_6} {γ : Type u_7} :
∀ {x : } {x_1 : } {f : αβ} {g : αγ}, Measurable fun (a : α) => (f a, g a)
theorem Measurable.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : } {mβ : } {mγ : } [] {f : αβ} {g : γδ} (hf : ) (hg : ) :
theorem measurable_prod_mk_left {α : Type u_1} {β : Type u_2} {m : } {mβ : } {x : α} :
theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} {m : } {mβ : } {y : β} :
Measurable fun (x : α) => (x, y)
theorem Measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβγ} (hf : ) {x : α} :
theorem Measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβγ} (hf : ) {y : β} :
Measurable fun (x : α) => f x y
theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } {mγ : } {f : αβ × γ} :
(Measurable fun (a : α) => (f a).1) Measurable fun (a : α) => (f a).2
theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : } {mβ : } :
Measurable Prod.swap
theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } :
∀ {x : } {f : α × βγ}, Measurable (f Prod.swap)
theorem MeasurableSet.prod {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem measurableSet_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set α} {t : Set β} (h : Set.Nonempty (s ×ˢ t)) :
theorem measurableSet_prod {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set α} {t : Set β} :
theorem measurableSet_swap_iff {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set (α × β)} :
MeasurableSet (Prod.swap ⁻¹' s)
instance Prod.instMeasurableSingletonClass {α : Type u_1} {β : Type u_2} {m : } {mβ : } :
Equations
• (_ : ) = (_ : )
theorem measurable_from_prod_countable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } [] :
∀ {x : } {f : α × βγ}, (∀ (y : β), Measurable fun (x : α) => f (x, y))
theorem Measurable.find {α : Type u_1} {β : Type u_2} {mβ : } :
∀ {x : } {f : αβ} {p : αProp} [inst : (n : ) → DecidablePred (p n)], (∀ (n : ), Measurable (f n))(∀ (n : ), MeasurableSet {x : α | p n x})∀ (h : ∀ (x : α), ∃ (n : ), p n x), Measurable fun (x : α) => f (Nat.find (_ : ∃ (n : ), p n x)) x

A piecewise function on countably many pieces is measurable if all the data is measurable.

theorem measurable_iUnionLift {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : } {mβ : } [] {t : ιSet α} {f : (i : ι) → (t i)β} (htf : ∀ (i j : ι) (x : α) (hxi : x t i) (hxj : x t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) {T : Set α} (hT : T ⋃ (i : ι), t i) (htm : ∀ (i : ι), MeasurableSet (t i)) (hfm : ∀ (i : ι), Measurable (f i)) :
Measurable (Set.iUnionLift t f htf T hT)

Let t i be a countable covering of a set T by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.iUnionLift t f _ _ : T → β, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

theorem measurable_liftCover {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : } {mβ : } [] (t : ιSet α) (htm : ∀ (i : ι), MeasurableSet (t i)) (f : (i : ι) → (t i)β) (hfm : ∀ (i : ι), Measurable (f i)) (hf : ∀ (i j : ι) (x : α) (hxi : x t i) (hxj : x t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) (htU : ⋃ (i : ι), t i = Set.univ) :

Let t i be a countable covering of α by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.liftCover t f _ _, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

theorem exists_measurable_piecewise {α : Type u_1} {β : Type u_2} {m : } {mβ : } {ι : Type u_6} [] [] (t : ιSet α) (t_meas : ∀ (n : ι), MeasurableSet (t n)) (g : ιαβ) (hg : ∀ (n : ι), Measurable (g n)) (ht : Pairwise fun (i j : ι) => Set.EqOn (g i) (g j) (t i t j)) :
∃ (f : αβ), ∀ (n : ι), Set.EqOn f (g n) (t n)

Let t i be a nonempty countable family of measurable sets in α. Let g i : α → β be a family of measurable functions such that g i agrees with g j on t i ∩ t j. Then there exists a measurable function f : α → β that agrees with each g i on t i.

We only need the assumption [Nonempty ι] to prove [Nonempty (α → β)].

@[deprecated exists_measurable_piecewise]
theorem exists_measurable_piecewise_nat {α : Type u_1} {β : Type u_2} {mβ : } {m : } (t : Set β) (t_meas : ∀ (n : ), MeasurableSet (t n)) (t_disj : Pairwise (Disjoint on t)) (g : βα) (hg : ∀ (n : ), Measurable (g n)) :
∃ (f : βα), ∀ (n : ), xt n, f x = g n x

Given countably many disjoint measurable sets t n and countably many measurable functions g n, one can construct a measurable function that coincides with g n on t n.

instance MeasurableSpace.pi {δ : Type u_4} {π : δType u_6} [m : (a : δ) → MeasurableSpace (π a)] :
MeasurableSpace ((a : δ) → π a)
Equations
theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} {π : δType u_6} [] [(a : δ) → MeasurableSpace (π a)] {g : α(a : δ) → π a} :
∀ (a : δ), Measurable fun (x : α) => g x a
theorem measurable_pi_apply {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (a : δ) :
Measurable fun (f : (a : δ) → π a) => f a
theorem Measurable.eval {α : Type u_1} {δ : Type u_4} {π : δType u_6} [] [(a : δ) → MeasurableSpace (π a)] {a : δ} {g : α(a : δ) → π a} (hg : ) :
Measurable fun (x : α) => g x a
theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {π : δType u_6} [] [(a : δ) → MeasurableSpace (π a)] (f : α(a : δ) → π a) (hf : ∀ (a : δ), Measurable fun (c : α) => f c a) :
theorem measurable_update' {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [] :
Measurable fun (p : ((i : δ) → π i) × π a) => Function.update p.1 a p.2

The function (f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a is measurable.

theorem measurable_uniqueElim {δ : Type u_4} {π : δType u_6} [] [(i : δ) → MeasurableSpace (π i)] :
Measurable uniqueElim
theorem measurable_updateFinset {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [] {s : } {x : (i : δ) → π i} :
theorem measurable_update {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [] :

The function update f a : π a → Π a, π a is always measurable. This doesn't require f to be measurable. This should not be confused with the statement that update f a x is measurable.

theorem measurable_update_left {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [] {x : π a} :
Measurable fun (x_1 : (a : δ) → π a) => Function.update x_1 a x
theorem measurable_eq_mp {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] {i : δ} {i' : δ} (h : i = i') :
Measurable (Eq.mp (_ : π i = π i'))
theorem Measurable.eq_mp {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] {β : Type u_7} [] {i : δ} {i' : δ} (h : i = i') {f : βπ i} (hf : ) :
Measurable fun (x : β) => Eq.mp (_ : π i = π i') (f x)
theorem measurable_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (f : δ' δ) :
theorem MeasurableSet.pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : ) (ht : is, MeasurableSet (t i)) :
theorem MeasurableSet.univ_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [] {t : (i : δ) → Set (π i)} (ht : ∀ (i : δ), MeasurableSet (t i)) :
MeasurableSet (Set.pi Set.univ t)
theorem measurableSet_pi_of_nonempty {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : ) (h : Set.Nonempty (Set.pi s t)) :
MeasurableSet (Set.pi s t) is, MeasurableSet (t i)
theorem measurableSet_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : ) :
MeasurableSet (Set.pi s t) (is, MeasurableSet (t i)) Set.pi s t =
instance Pi.instMeasurableSingletonClass {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [] [∀ (a : δ), ] :
MeasurableSingletonClass ((a : δ) → π a)
Equations
theorem measurable_piEquivPiSubtypeProd_symm {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [] :
Measurable .symm
theorem measurable_piEquivPiSubtypeProd {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [] :
instance TProd.instMeasurableSpace {δ : Type u_4} (π : δType u_6) [(x : δ) → MeasurableSpace (π x)] (l : List δ) :
Equations
theorem measurable_tProd_mk {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) :
theorem measurable_tProd_elim {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] [] {l : List δ} {i : δ} (hi : i l) :
Measurable fun (v : ) =>
theorem measurable_tProd_elim' {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] [] {l : List δ} (h : ∀ (i : δ), i l) :
theorem MeasurableSet.tProd {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) {s : (i : δ) → Set (π i)} (hs : ∀ (i : δ), MeasurableSet (s i)) :
instance Sum.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : ] [m₂ : ] :
Equations
theorem measurable_inl {α : Type u_1} {β : Type u_2} [] [] :
Measurable Sum.inl
theorem measurable_inr {α : Type u_1} {β : Type u_2} [] [] :
Measurable Sum.inr
theorem measurableSet_sum_iff {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set (α β)} :
MeasurableSet (Sum.inl ⁻¹' s) MeasurableSet (Sum.inr ⁻¹' s)
theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } :
∀ {x : } {f : α βγ}, Measurable (f Sum.inl)Measurable (f Sum.inr)
theorem Measurable.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : } {mβ : } :
∀ {x : } {f : αγ} {g : βγ}, Measurable (Sum.elim f g)
theorem Measurable.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : } {mβ : } :
∀ {x : } {x_1 : } {f : αβ} {g : γδ}, Measurable (Sum.map f g)
@[simp]
theorem measurableSet_inl_image {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set α} :
MeasurableSet (Sum.inl '' s)
theorem MeasurableSet.inl_image {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set α} :
MeasurableSet (Sum.inl '' s)

Alias of the reverse direction of measurableSet_inl_image.

@[simp]
theorem measurableSet_inr_image {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set β} :
MeasurableSet (Sum.inr '' s)
theorem MeasurableSet.inr_image {α : Type u_1} {β : Type u_2} {m : } {mβ : } {s : Set β} :
MeasurableSet (Sum.inr '' s)

Alias of the reverse direction of measurableSet_inr_image.

theorem measurableSet_range_inl {α : Type u_1} {β : Type u_2} {mβ : } [] :
theorem measurableSet_range_inr {α : Type u_1} {β : Type u_2} {mβ : } [] :
instance Sigma.instMeasurableSpace {α : Type u_7} {β : αType u_6} [m : (a : α) → MeasurableSpace (β a)] :
Equations
@[simp]
theorem measurableSet_setOf {α : Type u_1} [] {p : αProp} :
MeasurableSet {a : α | p a}
@[simp]
theorem measurable_mem {α : Type u_1} {s : Set α} [] :
(Measurable fun (x : α) => x s)
theorem Measurable.setOf {α : Type u_1} [] {p : αProp} :
MeasurableSet {a : α | p a}

Alias of the reverse direction of measurableSet_setOf.

theorem MeasurableSet.mem {α : Type u_1} {s : Set α} [] :
Measurable fun (x : α) => x s

Alias of the reverse direction of measurable_mem.

theorem Measurable.not {α : Type u_1} [] {p : αProp} (hp : ) :
Measurable fun (x : α) => ¬p x
theorem Measurable.and {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (hq : ) :
Measurable fun (a : α) => p a q a
theorem Measurable.or {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (hq : ) :
Measurable fun (a : α) => p a q a
theorem Measurable.imp {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (hq : ) :
Measurable fun (a : α) => p aq a
theorem Measurable.iff {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (hq : ) :
Measurable fun (a : α) => p a q a
theorem Measurable.forall {α : Type u_1} {ι : Sort uι} [] [] {p : ιαProp} (hp : ∀ (i : ι), Measurable (p i)) :
Measurable fun (a : α) => ∀ (i : ι), p i a
theorem Measurable.exists {α : Type u_1} {ι : Sort uι} [] [] {p : ιαProp} (hp : ∀ (i : ι), Measurable (p i)) :
Measurable fun (a : α) => ∃ (i : ι), p i a
instance Set.instMeasurableSpace {α : Type u_1} :

This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.

Equations
• Set.instMeasurableSpace = id inferInstance
instance Set.instMeasurableSingletonClass {α : Type u_1} [] :
Equations
• (_ : ) = (_ : )
theorem measurable_set_iff {α : Type u_1} {β : Type u_2} [] {g : βSet α} :
∀ (a : α), Measurable fun (x : β) => a g x
theorem measurable_set_mem {α : Type u_1} (a : α) :
Measurable fun (s : Set α) => a s
theorem measurable_set_not_mem {α : Type u_1} (a : α) :
Measurable fun (s : Set α) => as
theorem measurableSet_mem {α : Type u_1} (a : α) :
MeasurableSet {s : Set α | a s}
theorem measurableSet_not_mem {α : Type u_1} (a : α) :
MeasurableSet {s : Set α | as}
theorem measurable_compl {α : Type u_1} :
Measurable fun (x : Set α) => x
@[simp]
theorem MeasurableSpace.generateFrom_singleton {α : Type u_1} (s : Set α) :
= MeasurableSpace.comap (fun (x : α) => x s)

The sigma-algebra generated by a single set s is {∅, s, sᶜ, univ}.

structure MeasurableEmbedding {α : Type u_6} {β : Type u_7} [] [] (f : αβ) :

A map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting, MeasurableEmbedding.of_measurable_inverse_range, and MeasurableEmbedding.of_measurable_inverse.

One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its range and the range is a measurable set. One implication is formalized as MeasurableEmbedding.equivRange; the other one follows from MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and MeasurableEmbedding.comp.

• injective :

A measurable embedding is injective.

• measurable :

A measurable embedding is a measurable function.

• measurableSet_image' : ∀ ⦃s : Set α⦄, MeasurableSet (f '' s)

The image of a measurable set under a measurable embedding is a measurable set.

Instances For
theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {mα : } [] {f : αβ} (hf : ) {s : Set α} :
theorem MeasurableEmbedding.id {α : Type u_1} {mα : } :
theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } [] [] {f : αβ} {g : βγ} (hg : ) (hf : ) :
theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {mα : } {s : Set α} (hs : ) :
theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : } [] {f : αβ} (hf : ) :
theorem MeasurableEmbedding.measurableSet_preimage {α : Type u_1} {β : Type u_2} {mα : } [] {f : αβ} (hf : ) {s : Set β} :
theorem MeasurableEmbedding.measurable_rangeSplitting {α : Type u_1} {β : Type u_2} {mα : } [] {f : αβ} (hf : ) :
theorem MeasurableEmbedding.measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } [] [] {f : αβ} (hf : ) {g : αγ} {g' : βγ} (hg : ) (hg' : ) :
theorem MeasurableEmbedding.exists_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } [] [] {f : αβ} (hf : ) {g : αγ} (hg : ) (hne : β) :
∃ (g' : βγ), g' f = g
theorem MeasurableEmbedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : } [] [] {f : αβ} {g : βγ} (hg : ) :
theorem MeasurableSet.exists_measurable_proj {α : Type u_1} :
∀ {x : } {s : Set α}, ∃ (f : αs), ∀ (x : s), f x = x
structure MeasurableEquiv (α : Type u_6) (β : Type u_7) [] [] extends :
Type (max u_6 u_7)

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

• toFun : αβ
• invFun : βα
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• measurable_toFun : Measurable self.toEquiv

The forward function of a measurable equivalence is measurable.

• measurable_invFun : Measurable self.symm

The inverse function of a measurable equivalence is measurable.

Instances For

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

Equations
Instances For
theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [] [] :
Function.Injective MeasurableEquiv.toEquiv
instance MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [] [] :
EquivLike (α ≃ᵐ β) α β
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.toEquiv = e
theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
@[simp]
theorem MeasurableEquiv.coe_mk {α : Type u_1} {β : Type u_2} [] [] (e : α β) (h1 : ) (h2 : Measurable e.symm) :
{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = e
def MeasurableEquiv.refl (α : Type u_6) [] :
α ≃ᵐ α

Any measurable space is equivalent to itself.

Equations
• = { toEquiv := , measurable_toFun := (_ : ), measurable_invFun := (_ : ) }
Instances For
instance MeasurableEquiv.instInhabited {α : Type u_1} [] :
Equations
• MeasurableEquiv.instInhabited = { default := }
def MeasurableEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
α ≃ᵐ γ

The composition of equivalences between measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
(ab.trans bc) = bc ab
def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [] [] (ab : α ≃ᵐ β) :
β ≃ᵐ α

The inverse of an equivalence between measurable spaces.

Equations
• ab.symm = { toEquiv := ab.symm, measurable_toFun := (_ : Measurable ab.symm), measurable_invFun := (_ : Measurable ab.toEquiv) }
Instances For
@[simp]
theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.symm = e.symm
def MeasurableEquiv.Simps.apply {α : Type u_1} {β : Type u_2} [] [] (h : α ≃ᵐ β) :
αβ

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
Instances For
def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [] [] (h : α ≃ᵐ β) :
βα

See Note [custom simps projection]

Equations
• = h.symm
Instances For
theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [] [] {e₁ : α ≃ᵐ β} {e₂ : α ≃ᵐ β} (h : e₁ = e₂) :
e₁ = e₂
@[simp]
theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [] [] (e : α β) (h1 : ) (h2 : Measurable e.symm) :
{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }
@[simp]
theorem MeasurableEquiv.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
(ab.trans bc).toEquiv = ab.trans bc.toEquiv
@[simp]
theorem MeasurableEquiv.refl_toEquiv (α : Type u_6) [] :
.toEquiv =
@[simp]
theorem MeasurableEquiv.refl_apply (α : Type u_6) [] (a : α) :
a = a
@[simp]
theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
∀ (a : α), (ab.trans bc) a = bc (ab a)
@[simp]
theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.symm.symm = e
theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [] [] :
Function.Bijective MeasurableEquiv.symm
@[simp]
theorem MeasurableEquiv.symm_refl (α : Type u_6) [] :
.symm =
@[simp]
theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.symm e = id
@[simp]
theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e e.symm = id
@[simp]
theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (y : β) :
e (e.symm y) = y
@[simp]
theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (x : α) :
e.symm (e x) = x
@[simp]
theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.symm.trans e =
@[simp]
theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
e.trans e.symm =
theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
@[simp]
theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set β) :
e.symm ⁻¹' (e ⁻¹' s) = s
theorem MeasurableEquiv.image_eq_preimage {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set α) :
e '' s = e.symm ⁻¹' s
theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set α) :
e.symm ⁻¹' s = e '' s
theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set β) :
e.symm '' s = e ⁻¹' s
theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set β) (t : Set α) :
s = e '' t e.symm '' s = t
@[simp]
theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set β) :
e '' (e ⁻¹' s) = s
@[simp]
theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) (s : Set α) :
e ⁻¹' (e '' s) = s
@[simp]
theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) {s : Set β} :
@[simp]
theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) {s : Set α} :
MeasurableSet (e '' s)
@[simp]
theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :
MeasurableSpace.map (e) inst✝¹ = inst✝
theorem MeasurableEquiv.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) :

A measurable equivalence is a measurable embedding.

def MeasurableEquiv.cast {α : Type u_6} {β : Type u_6} [i₁ : ] [i₂ : ] (h : α = β) (hi : HEq i₁ i₂) :
α ≃ᵐ β

Equal measurable spaces are equivalent.

Equations
• = { toEquiv := , measurable_toFun := (_ : Measurable ()), measurable_invFun := (_ : Measurable ().symm) }
Instances For
def MeasurableEquiv.ulift {α : Type u} [] :
≃ᵐ α

Measurable equivalence between ULift α and α.

Equations
• MeasurableEquiv.ulift = { toEquiv := Equiv.ulift, measurable_toFun := (_ : Measurable ULift.down), measurable_invFun := (_ : Measurable ULift.up) }
Instances For
theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : βγ} (e : α ≃ᵐ β) :
Measurable (f e)
def MeasurableEquiv.ofUniqueOfUnique (α : Type u_6) (β : Type u_7) [] [] [] [] :
α ≃ᵐ β

Any two types with unique elements are measurably equivalent.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
α × γ ≃ᵐ β × δ

Products of equivalent measurable spaces are equivalent.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [] [] :
α × β ≃ᵐ β × α

Products of measurable spaces are symmetric.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] :
(α × β) × γ ≃ᵐ α × β × γ

Products of measurable spaces are associative.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
α γ ≃ᵐ β δ

Sums of measurable spaces are symmetric.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.Set.prod {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (t : Set β) :
(s ×ˢ t) ≃ᵐ s × t

s ×ˢ t ≃ (s × t) as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.Set.univ (α : Type u_6) [] :
Set.univ ≃ᵐ α

univ α ≃ α as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.Set.singleton {α : Type u_1} [] (a : α) :
{a} ≃ᵐ Unit

{a} ≃ Unit as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.Set.rangeInl {α : Type u_1} {β : Type u_2} [] [] :
(Set.range Sum.inl) ≃ᵐ α

α is equivalent to its image in α ⊕ β as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.Set.rangeInr {α : Type u_1} {β : Type u_2} [] [] :
(Set.range Sum.inr) ≃ᵐ β

β is equivalent to its image in α ⊕ β as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [] [] [] :
(α β) × γ ≃ᵐ α × γ β × γ

Products distribute over sums (on the right) as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [] [] [] :
α × (β γ) ≃ᵐ α × β α × γ

Products distribute over sums (on the left) as measurable spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [] [] [] [] :
(α β) × (γ δ) ≃ᵐ (α × γ α × δ) β × γ β × δ

Products distribute over sums as measurable spaces.

Equations
Instances For
def MeasurableEquiv.piCongrRight {δ' : Type u_5} {π : δ'Type u_6} {π' : δ'Type u_7} [(x : δ') → MeasurableSpace (π x)] [(x : δ') → MeasurableSpace (π' x)] (e : (a : δ') → π a ≃ᵐ π' a) :
((a : δ') → π a) ≃ᵐ ((a : δ') → π' a)

A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence between Π a, β₁ a and Π a, β₂ a.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.piCongrLeft {δ : Type u_4} {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (f : δ δ') :
((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)

Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : δ δ') :
= ()
@[simp]
theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [] {l : List δ'} (hnd : ) (h : ∀ (i : δ'), i l) :
.symm =
@[simp]
theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [] {l : List δ'} (hnd : ) (h : ∀ (i : δ'), i l) :
def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ'Type u_6} [(x : δ') → MeasurableSpace (π x)] [] {l : List δ'} (hnd : ) (h : ∀ (i : δ'), i l) :
((i : δ') → π i) ≃ᵐ

Pi-types are measurably equivalent to iterated products.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
= fun (f : (i : δ') → π i) => f default
@[simp]
theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
.symm = uniqueElim
def MeasurableEquiv.piUnique {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :
((i : δ') → π i) ≃ᵐ π default

The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains ⋆

Equations
• = { toEquiv := , measurable_toFun := (_ : Measurable fun (f : (a : δ') → π a) => f default), measurable_invFun := (_ : Measurable uniqueElim) }
Instances For
@[simp]
theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [] [] :
.symm = uniqueElim
@[simp]
theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [] [] :
= fun (f : αβ) => f default
def MeasurableEquiv.funUnique (α : Type u_8) (β : Type u_9) [] [] :
(αβ) ≃ᵐ β

If α has a unique term, then the type of function α → β is measurably equivalent to β.

Equations
Instances For
@[simp]
theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
= fun (f : (i : Fin 2) → α i) => (f 0, f 1)
@[simp]
theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
.symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
def MeasurableEquiv.piFinTwo (α : Fin 2Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :
((i : Fin 2) → α i) ≃ᵐ α 0 × α 1

The space Π i : Fin 2, α i is measurably equivalent to α 0 × α 1.

Equations
• = { toEquiv := , measurable_toFun := (_ : ), measurable_invFun := (_ : Measurable ().symm) }
Instances For
@[simp]
theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [] :
MeasurableEquiv.finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
@[simp]
theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [] :
MeasurableEquiv.finTwoArrow = fun (f : Fin 2α) => (f 0, f 1)
def MeasurableEquiv.finTwoArrow {α : Type u_1} [] :
(Fin 2α) ≃ᵐ α × α

The space Fin 2 → α is measurably equivalent to α × α.

Equations
Instances For
@[simp]
theorem MeasurableEquiv.piFinSuccAbove_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
= fun (f : (j : Fin (n + 1)) → α j) => (f i, fun (j : Fin n) => f ())
@[simp]
theorem MeasurableEquiv.piFinSuccAbove_symm_apply {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
.symm = fun (f : α i × ((j : Fin n) → α ())) => Fin.insertNth i f.1 f.2
def MeasurableEquiv.piFinSuccAbove {n : } (α : Fin (n + 1)Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :
((j : Fin (n + 1)) → α j) ≃ᵐ α i × ((j : Fin n) → α ())

Measurable equivalence between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [] :
= fun (f : (i : δ') → π i) => (fun (x : { x : δ' // p x }) => f x, fun (x : { x : δ' // ¬p x }) => f x)
@[simp]
theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [] :
.symm = fun (f : ((i : { x : δ' // p x }) → π i) × ((i : { x : δ' // ¬p x }) → π i)) (x : δ') => if h : p x then f.fst { val := x, property := h } else f.snd { val := x, property := h }
def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ'Prop) [] :
((i : δ') → π i) ≃ᵐ ((i : ) → π i) × ((i : { i : δ' // ¬p i }) → π i)

Measurable equivalence between (dependent) functions on a type and pairs of functions on {i // p i} and {i // ¬p i}. See also Equiv.piEquivPiSubtypeProd.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
((i : δ δ') → α i) ≃ᵐ ((i : δ) → α ()) × ((i' : δ') → α (Sum.inr i'))

The measurable equivalence between the pi type over a sum type and a product of pi-types. This is similar to MeasurableEquiv.piEquivPiSubtypeProd.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : δ δ'Type u_8) [(i : δ δ') → MeasurableSpace (α i)] :
.symm = .symm
def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ'Type u_6) [(x : δ') → MeasurableSpace (π x)] [] {s : Finset δ'} {t : Finset δ'} (h : Disjoint s t) :
((i : { x : δ' // x s }) → π i) × ((i : { x : δ' // x t }) → π i) ≃ᵐ ((i : { x : δ' // x s t }) → π i)

The measurable equivalence (∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i) for disjoint finsets s and t. Equiv.piFinsetUnion as a measurable equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasurableEquiv.sumCompl {α : Type u_1} [] {s : Set α} [DecidablePred fun (x : α) => x s] (hs : ) :
s s ≃ᵐ α

If s is a measurable set in a measurable space, that space is equivalent to the sum of s and sᶜ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasurableEquiv.ofInvolutive_toEquiv {α : Type u_1} [] (f : αα) (hf : ) (hf' : ) :
().toEquiv =
def MeasurableEquiv.ofInvolutive {α : Type u_1} [] (f : αα) (hf : ) (hf' : ) :
α ≃ᵐ α

Convert a measurable involutive function f to a measurable permutation with toFun = invFun = f. See also Function.Involutive.toPerm.

Equations
• = { toEquiv := , measurable_toFun := hf', measurable_invFun := hf' }
Instances For
@[simp]
theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [] (f : αα) (hf : ) (hf' : ) (a : α) :
() a = f a
@[simp]
theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [] (f : αα) (hf : ) (hf' : ) :
().symm =
@[simp]
theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
MeasurableSpace.comap f inst✝ = inst✝¹
theorem MeasurableEmbedding.iff_comap_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
MeasurableSpace.comap f inst✝ = inst✝¹
noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (s : Set α) (hf : ) :
s ≃ᵐ (f '' s)

A set is equivalent to its image under a function f as measurable spaces, if f is a measurable embedding

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MeasurableEmbedding.equivRange {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
α ≃ᵐ ()

The domain of f is equivalent to its range as measurable spaces, if f is a measurable embedding

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableEmbedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : ()α} (hf₁ : ) (hf₂ : ) (hg : ) (H : ) :
theorem MeasurableEmbedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} (hf₁ : ) (hf₂ : ) (hg : ) (H : ) :
noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} (hf : ) (hg : ) :
α ≃ᵐ β

The measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasurableSpace.comap_compl {α : Type u_1} {β : Type u_2} {m' : } [] (h : Measurable compl) (f : αβ) :
MeasurableSpace.comap (fun (a : α) => (f a)) inferInstance = MeasurableSpace.comap f inferInstance
@[simp]
theorem MeasurableSpace.comap_not {α : Type u_1} (p : αProp) :
MeasurableSpace.comap (fun (a : α) => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance

We say a measurable space is countably generated if it can be generated by a countable set of sets.

• isCountablyGenerated : ∃ (b : Set (Set α)),
Instances
theorem MeasurableSpace.CountablyGenerated.comap {α : Type u_1} {β : Type u_2} [m : ] (f : αβ) :
theorem MeasurableSpace.CountablyGenerated.sup {β : Type u_2} {m₁ : } {m₂ : } :
instance MeasurableSpace.instCountablyGenerated {α : Type u_1} [] [] :
Equations
Equations
• (_ : ) = (_ : )
Equations
theorem MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated (α : Type u_1) [] [HasCountableSeparatingOn α MeasurableSet Set.univ] :
∃ (f : α),

If a measurable space is countably generated and separates points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

class Filter.IsMeasurablyGenerated {α : Type u_1} [] (f : ) :

A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.

• exists_measurable_subset : ∀ ⦃s : Set α⦄, s f∃ t ∈ f, t s
Instances
instance Filter.isMeasurablyGenerated_bot {α : Type u_1} [] :
Equations
instance Filter.isMeasurablyGenerated_top {α : Type u_1} [] :
Equations
theorem Filter.Eventually.exists_measurable_mem {α : Type u_1} [] {f : } {p : αProp} (h : ∀ᶠ (x : α) in f, p x) :
∃ s ∈ f, xs, p x
theorem Filter.Eventually.exists_measurable_mem_of_smallSets {α : Type u_1} [] {f : } {p : Set αProp} (h : ∀ᶠ (s : Set α) in , p s) :
∃ s ∈ f, p s
instance Filter.inf_isMeasurablyGenerated {α : Type u_1} [] (f : ) (g : ) :
Equations
• (_ : ) = (_ : )
theorem MeasurableSet.principal_isMeasurablyGenerated {α : Type u_1} [] {s : Set α} :

Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff.

instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [] {f : ι} [∀ (i : ι), ] :
Filter.IsMeasurablyGenerated (⨅ (i : ι), f i)
Equations
theorem measurableSet_tendsto {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
∀ {x : } [inst : ] [inst_1 : ] {l : } [inst_2 : ] (l' : ) [inst_3 : ] [hl' : ] {f : δβγ}, (∀ (i : δ), Measurable (f i))MeasurableSet {x : β | Filter.Tendsto (fun (n : δ) => f n x) l l'}

The set of points for which a sequence of measurable functions converges to a given value is measurable.

def IsCountablySpanning {α : Type u_1} (C : Set (Set α)) :

We say that a collection of sets is countably spanning if a countable subset spans the whole type. This is a useful condition in various parts of measure theory. For example, it is a needed condition to show that the product of two collections generate the product sigma algebra, see generateFrom_prod_eq.

Equations
Instances For

### Typeclasses on Subtype MeasurableSet#

instance MeasurableSet.Subtype.instMembership {α : Type u_1} [] :
Membership α (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instMembership = { mem := fun (a : α) (s : Subtype MeasurableSet) => a s }
@[simp]
theorem MeasurableSet.mem_coe {α : Type u_1} [] (a : α) (s : Subtype MeasurableSet) :
a s a s
Equations
• MeasurableSet.Subtype.instEmptyCollection = { emptyCollection := { val := , property := (_ : ) } }
@[simp]
theorem MeasurableSet.coe_empty {α : Type u_1} [] :
=
instance MeasurableSet.Subtype.instInsert {α : Type u_1} [] :
Insert α (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instInsert = { insert := fun (a : α) (s : Subtype MeasurableSet) => { val := insert a s, property := (_ : MeasurableSet (insert a s)) } }
@[simp]
theorem MeasurableSet.coe_insert {α : Type u_1} [] (a : α) (s : Subtype MeasurableSet) :
(insert a s) = insert a s
instance MeasurableSet.Subtype.instSingleton {α : Type u_1} [] :
Singleton α (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => { val := {a}, property := (_ : ) } }
@[simp]
theorem MeasurableSet.coe_singleton {α : Type u_1} [] (a : α) :
{a} = {a}
Equations
instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [] :
HasCompl (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instHasCompl = { compl := fun (x : Subtype MeasurableSet) => { val := (x), property := (_ : MeasurableSet (x)) } }
@[simp]
theorem MeasurableSet.coe_compl {α : Type u_1} [] (s : Subtype MeasurableSet) :
s = (s)
instance MeasurableSet.Subtype.instUnion {α : Type u_1} [] :
Union (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instUnion = { union := fun (x y : Subtype MeasurableSet) => { val := x y, property := (_ : MeasurableSet (x y)) } }
@[simp]
theorem MeasurableSet.coe_union {α : Type u_1} [] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
(s t) = s t
instance MeasurableSet.Subtype.instSup {α : Type u_1} [] :
Sup (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instSup = { sup := fun (x y : Subtype MeasurableSet) => x y }
@[simp]
theorem MeasurableSet.sup_eq_union {α : Type u_1} [] (s : { s : Set α // }) (t : { s : Set α // }) :
s t = s t
instance MeasurableSet.Subtype.instInter {α : Type u_1} [] :
Inter (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instInter = { inter := fun (x y : Subtype MeasurableSet) => { val := x y, property := (_ : MeasurableSet (x y)) } }
@[simp]
theorem MeasurableSet.coe_inter {α : Type u_1} [] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
(s t) = s t
instance MeasurableSet.Subtype.instInf {α : Type u_1} [] :
Inf (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instInf = { inf := fun (x y : Subtype MeasurableSet) => x y }
@[simp]
theorem MeasurableSet.inf_eq_inter {α : Type u_1} [] (s : { s : Set α // }) (t : { s : Set α // }) :
s t = s t
instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [] :
SDiff (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instSDiff = { sdiff := fun (x y : Subtype MeasurableSet) => { val := x \ y, property := (_ : MeasurableSet (x \ y)) } }
@[simp]
theorem MeasurableSet.coe_sdiff {α : Type u_1} [] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
(s \ t) = s \ t
instance MeasurableSet.Subtype.instBot {α : Type u_1} [] :
Bot (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instBot = { bot := }
@[simp]
theorem MeasurableSet.coe_bot {α : Type u_1} [] :
=
instance MeasurableSet.Subtype.instTop {α : Type u_1} [] :
Top (Subtype MeasurableSet)
Equations
• MeasurableSet.Subtype.instTop = { top := { val := Set.univ, property := (_ : MeasurableSet Set.univ) } }
@[simp]
theorem MeasurableSet.coe_top {α : Type u_1} [] :
=
Equations
• One or more equations did not get rendered due to their size.
theorem MeasurableSet.measurableSet_blimsup {α : Type u_1} [] {s : Set α} {p : } (h : ∀ (n : ), p nMeasurableSet (s n)) :
MeasurableSet (Filter.blimsup s Filter.atTop p)
theorem MeasurableSet.measurableSet_bliminf {α : Type u_1} [] {s : Set α} {p : } (h : ∀ (n : ), p nMeasurableSet (s n)) :
MeasurableSet (Filter.bliminf s Filter.atTop p)
theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
MeasurableSet (Filter.limsup s Filter.atTop)
theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
MeasurableSet (Filter.liminf s Filter.atTop)