# mathlibdocumentation

measure_theory.measurable_space

# 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 `measure_theory.measurable_space_def`.

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

@[protected]
def measurable_space.map {α : Type u_1} {β : Type u_2} (f : α → β) (m : measurable_space α) :

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
@[simp]
theorem measurable_space.map_id {α : Type u_1} {m : measurable_space α} :
@[simp]
theorem measurable_space.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {f : α → β} {g : β → γ} :
@[protected]
def measurable_space.comap {α : Type u_1} {β : Type u_2} (f : α → β) (m : measurable_space β) :

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
theorem measurable_space.comap_eq_generate_from {α : Type u_1} {β : Type u_2} (m : measurable_space β) (f : α → β) :
= measurable_space.generate_from {t : set α | ∃ (s : set β), f ⁻¹' s = t}
@[simp]
theorem measurable_space.comap_id {α : Type u_1} {m : measurable_space α} :
@[simp]
theorem measurable_space.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {f : β → α} {g : γ → β} :
theorem measurable_space.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {m' : measurable_space β} {f : α → β} :
m m'
theorem measurable_space.gc_comap_map {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem measurable_space.map_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {f : α → β} (h : m₁ m₂) :
theorem measurable_space.monotone_map {α : Type u_1} {β : Type u_2} {f : α → β} :
theorem measurable_space.comap_mono {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {g : β → α} (h : m₁ m₂) :
theorem measurable_space.monotone_comap {α : Type u_1} {β : Type u_2} {g : β → α} :
@[simp]
theorem measurable_space.comap_bot {α : Type u_1} {β : Type u_2} {g : β → α} :
@[simp]
theorem measurable_space.comap_sup {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {g : β → α} :
(m₁ m₂) =
@[simp]
theorem measurable_space.comap_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {g : β → α} {m : ι → } :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
@[simp]
theorem measurable_space.map_top {α : Type u_1} {β : Type u_2} {f : α → β} :
@[simp]
theorem measurable_space.map_inf {α : Type u_1} {β : Type u_2} {m₁ m₂ : measurable_space α} {f : α → β} :
(m₁ m₂) =
@[simp]
theorem measurable_space.map_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : α → β} {m : ι → } :
(⨅ (i : ι), m i) = ⨅ (i : ι), (m i)
theorem measurable_space.comap_map_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : α → β} :
theorem measurable_space.le_map_comap {α : Type u_1} {β : Type u_2} {m : measurable_space α} {g : β → α} :
theorem measurable_space.comap_generate_from {α : Type u_1} {β : Type u_2} {f : α → β} {s : set (set β)} :
theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₂
theorem measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₂

Alias of the forward direction of `measurable_iff_le_map`.

theorem measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₂

Alias of the reverse direction of `measurable_iff_le_map`.

theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₁
theorem measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₁

Alias of the forward direction of `measurable_iff_comap_le`.

theorem measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
m₁

Alias of the reverse direction of `measurable_iff_comap_le`.

theorem measurable.mono {α : Type u_1} {β : Type u_2} {ma ma' : measurable_space α} {mb mb' : measurable_space β} {f : α → β} (hf : measurable f) (ha : ma ma') (hb : mb' mb) :
@[measurability]
theorem measurable_from_top {α : Type u_1} {β : Type u_2} {f : α → β} :
theorem measurable_generate_from {α : Type u_1} {β : Type u_2} {s : set (set β)} {f : α → β} (h : ∀ (t : set β), t smeasurable_set (f ⁻¹' t)) :
@[measurability]
theorem subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : α → β} [subsingleton α] :
@[measurability]
theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [subsingleton β] (f : α → β) :
theorem measurable_zero {α : Type u_1} {β : Type u_2} [has_zero α] :
theorem measurable_one {α : Type u_1} {β : Type u_2} [has_one α] :
theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [is_empty α] (f : α → β) :
theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [is_empty β] (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_of_finite {α : Type u_1} {β : Type u_2} [finite α] (f : α → β) :
@[measurability]
theorem measurable.iterate {α : Type u_1} {m : measurable_space α} {f : α → α} (hf : measurable f) (n : ) :
@[measurability]
theorem measurable_set_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} {mβ : measurable_space β} {t : set β} (hf : measurable f) (ht : measurable_set t) :
@[measurability]
theorem measurable.piecewise {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} {m : measurable_space α} {mβ : measurable_space β} {_x : decidable_pred (λ (_x : α), _x s)} (hs : measurable_set s) (hf : measurable f) (hg : measurable g) :
theorem measurable.ite {α : Type u_1} {β : Type u_2} {f g : α → β} {m : measurable_space α} {mβ : measurable_space β} {p : α → Prop} {_x : decidable_pred p} (hp : measurable_set {a : α | p a}) (hf : measurable f) (hg : measurable g) :
measurable (λ (x : α), ite (p x) (f x) (g x))

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

@[measurability]
theorem measurable.indicator {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} {m : measurable_space α} {mβ : measurable_space β} [has_zero β] (hf : measurable f) (hs : measurable_set s) :
@[measurability]
theorem measurable_set_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} {mβ : measurable_space β} [has_zero β] (hf : measurable f) :
@[measurability]
theorem measurable_set_mul_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} {mβ : measurable_space β} [has_one β] (hf : measurable f) :
theorem measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f g : α → β} {m : measurable_space α} {mβ : measurable_space β} (hf : measurable f) (h : {x : α | f x g x}.countable) :

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [countable α] {f : β → α} (h : ∀ (y : β), measurable_set (f ⁻¹' {f y})) :
@[measurability]
theorem measurable_unit {α : Type u_1} (f : unit → α) :
@[measurability]
theorem measurable_from_nat {α : Type u_1} {f : → α} :
theorem measurable_to_nat {α : Type u_1} {f : α → } :
(∀ (y : α), measurable_set (f ⁻¹' {f y}))
theorem measurable_find_greatest' {α : Type u_1} {p : α → → Prop} [Π (x : α), decidable_pred (p x)] {N : } (hN : ∀ (k : ), k Nmeasurable_set {x : α | nat.find_greatest (p x) N = k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem measurable_find_greatest {α : Type u_1} {p : α → → Prop} [Π (x : α), decidable_pred (p x)] {N : } (hN : ∀ (k : ), k Nmeasurable_set {x : α | p x k}) :
measurable (λ (x : α), nat.find_greatest (p x) N)
theorem measurable_find {α : Type u_1} {p : α → → Prop} [Π (x : α), decidable_pred (p x)] (hp : ∀ (x : α), ∃ (N : ), p x N) (hm : ∀ (k : ), measurable_set {x : α | p x k}) :
measurable (λ (x : α), nat.find _)
@[protected, instance]
def quot.measurable_space {α : Type u_1} {r : α → α → Prop} [m : measurable_space α] :
Equations
@[protected, instance]
def quotient.measurable_space {α : Type u_1} {s : setoid α} [m : measurable_space α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def quotient_group.measurable_space {G : Type u_1} [group G] (S : subgroup G) :
Equations
theorem measurable_set_quotient {α : Type u_1} {s : setoid α} {t : set (quotient s)} :
theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} {s : setoid α} {f : → β} :
@[measurability]
theorem measurable_quotient_mk {α : Type u_1} [s : setoid α] :
@[measurability]
theorem measurable_quotient_mk' {α : Type u_1} {s : setoid α} :
@[measurability]
theorem measurable_quot_mk {α : Type u_1} {r : α → α → Prop} :
measurable (quot.mk r)
@[measurability]
@[measurability]
theorem quotient_group.measurable_coe {G : Type u_1} [group G] {S : subgroup G} :
theorem quotient_add_group.measurable_from_quotient {α : Type u_1} {G : Type u_2} [add_group G] {S : add_subgroup G} {f : G S → α} :
theorem quotient_group.measurable_from_quotient {α : Type u_1} {G : Type u_2} [group G] {S : subgroup G} {f : G S → α} :
@[protected, instance]
def subtype.measurable_space {α : Type u_1} {p : α → Prop} [m : measurable_space α] :
Equations
@[measurability]
theorem measurable_subtype_coe {α : Type u_1} {p : α → Prop} :
@[protected, instance]
def subtype.measurable_singleton_class {α : Type u_1} {p : α → Prop}  :
theorem measurable_set.subtype_image {α : Type u_1} {m : measurable_space α} {s : set α} {t : set s} (hs : measurable_set s) :
@[measurability]
theorem measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {p : β → Prop} {f : α → } (hf : measurable f) :
measurable (λ (a : α), (f a))
@[measurability]
theorem measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {p : β → Prop} {f : α → β} (hf : measurable f) {h : ∀ (x : α), p (f x)} :
measurable (λ (x : α), f x, _⟩)
theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {f : α → β} (s t : set α) (hs : measurable_set s) (ht : measurable_set t) (h : set.univ s t) (hc : measurable (λ (a : s), f a)) (hd : measurable (λ (a : t), f a)) :
theorem measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {f : α → β} {s : set α} (hs : measurable_set s) (h₁ : measurable (s.restrict f)) (h₂ : measurable (s.restrict f)) :
theorem measurable.dite {α : Type u_1} {β : Type u_2} {s : set α} {m : measurable_space α} {mβ : measurable_space β} [Π (x : α), decidable (x s)] {f : s → β} (hf : measurable f) {g : s → β} (hg : measurable g) (hs : measurable_set s) :
measurable (λ (x : α), dite (x s) (λ (hx : x s), f x, hx⟩) (λ (hx : x s), g x, hx⟩))
theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {f : α → β} (s : set α) (hs : s.finite) (hf : measurable (s.restrict f)) :
theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {f : α → β} (a : α) (hf : measurable ({x : α | x a}.restrict f)) :
def measurable_space.prod {α : Type u_1} {β : Type u_2} (m₁ : measurable_space α) (m₂ : measurable_space β) :

A `measurable_space` structure on the product of two measurable spaces.

Equations
@[protected, instance]
def prod.measurable_space {α : Type u_1} {β : Type u_2} [m₁ : measurable_space α] [m₂ : measurable_space β] :
Equations
@[measurability]
theorem measurable_fst {α : Type u_1} {β : Type u_2} {ma : measurable_space α} {mb : measurable_space β} :
@[measurability]
theorem measurable_snd {α : Type u_1} {β : Type u_2} {ma : measurable_space α} {mb : measurable_space β} :
theorem measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β × γ} (hf : measurable f) :
measurable (λ (a : α), (f a).fst)
theorem measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β × γ} (hf : measurable f) :
measurable (λ (a : α), (f a).snd)
@[measurability]
theorem measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β × γ} (hf₁ : measurable (λ (a : α), (f a).fst)) (hf₂ : measurable (λ (a : α), (f a).snd)) :
theorem measurable.prod_mk {α : Type u_1} {m : measurable_space α} {β : Type u_2} {γ : Type u_3} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : α), (f a, g a))
theorem measurable.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β} {g : γ → δ} (hf : measurable f) (hg : measurable g) :
theorem measurable_prod_mk_left {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {x : α} :
theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {y : β} :
measurable (λ (x : α), (x, y))
theorem measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β → γ} (hf : measurable ) {x : α} :
theorem measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β → γ} (hf : measurable ) {y : β} :
measurable (λ (x : α), f x y)
theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → β × γ} :
measurable (λ (a : α), (f a).fst) measurable (λ (a : α), (f a).snd)
@[measurability]
theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} :
theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α × β → γ} :
@[measurability]
theorem measurable_set.prod {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set α} {t : set β} (hs : measurable_set s) (ht : measurable_set t) :
theorem measurable_set_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set α} {t : set β} (h : (s ×ˢ t).nonempty) :
theorem measurable_set_prod {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set α} {t : set β} :
theorem measurable_set_swap_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set × β)} :
theorem measurable_from_prod_countable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} [countable β] {mγ : measurable_space γ} {f : α × β → γ} (hf : ∀ (y : β), measurable (λ (x : α), f (x, y))) :
@[measurability]
theorem measurable.find {α : Type u_1} {β : Type u_2} {mβ : measurable_space β} {m : measurable_space α} {f : α → β} {p : α → Prop} [Π (n : ), decidable_pred (p n)] (hf : ∀ (n : ), measurable (f n)) (hp : ∀ (n : ), measurable_set {x : α | p n x}) (h : ∀ (x : α), ∃ (n : ), p n x) :
measurable (λ (x : α), f (nat.find _) x)

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

theorem exists_measurable_piecewise_nat {α : Type u_1} {β : Type u_2} {mβ : measurable_space β} {m : measurable_space α} (t : set β) (t_meas : ∀ (n : ), measurable_set (t n)) (t_disj : pairwise (disjoint on t)) (g : β → α) (hg : ∀ (n : ), measurable (g n)) :
∃ (f : β → α), ∀ (n : ) (x : β), x t nf 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`.

@[protected, instance]
def measurable_space.pi {δ : Type u_4} {π : δ → Type u_7} [m : Π (a : δ), measurable_space (π a)] :
measurable_space (Π (a : δ), π a)
Equations
theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] {g : α → Π (a : δ), π a} :
∀ (a : δ), measurable (λ (x : α), g x a)
@[measurability]
theorem measurable_pi_apply {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] (a : δ) :
measurable (λ (f : Π (a : δ), π a), f a)
@[measurability]
theorem measurable.eval {α : Type u_1} {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] {a : δ} {g : α → Π (a : δ), π a} (hg : measurable g) :
measurable (λ (x : α), g x a)
@[measurability]
theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] (f : α → Π (a : δ), π a) (hf : ∀ (a : δ), measurable (λ (c : α), f c a)) :
@[measurability]
theorem measurable_update {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] (f : Π (a : δ), π a) {a : δ} [decidable_eq δ] :

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.

@[measurability]
theorem measurable_set.pi {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] {s : set δ} {t : Π (i : δ), set (π i)} (hs : s.countable) (ht : ∀ (i : δ), i smeasurable_set (t i)) :
theorem measurable_set.univ_pi {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] [countable δ] {t : Π (i : δ), set (π i)} (ht : ∀ (i : δ), measurable_set (t i)) :
theorem measurable_set_pi_of_nonempty {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] {s : set δ} {t : Π (i : δ), set (π i)} (hs : s.countable) (h : (s.pi t).nonempty) :
measurable_set (s.pi t) ∀ (i : δ), i smeasurable_set (t i)
theorem measurable_set_pi {δ : Type u_4} {π : δ → Type u_7} [Π (a : δ), measurable_space (π a)] {s : set δ} {t : Π (i : δ), set (π i)} (hs : s.countable) :
measurable_set (s.pi t) (∀ (i : δ), i smeasurable_set (t i)) s.pi t =
@[measurability]
theorem measurable_pi_equiv_pi_subtype_prod_symm {δ : Type u_4} (π : δ → Type u_7) [Π (a : δ), measurable_space (π a)] (p : δ → Prop)  :
@[measurability]
theorem measurable_pi_equiv_pi_subtype_prod {δ : Type u_4} (π : δ → Type u_7) [Π (a : δ), measurable_space (π a)] (p : δ → Prop)  :
@[protected, instance]
def tprod.measurable_space {δ : Type u_4} (π : δ → Type u_1) [Π (x : δ), measurable_space (π x)] (l : list δ) :
Equations
theorem measurable_tprod_mk {δ : Type u_4} {π : δ → Type u_7} [Π (x : δ), measurable_space (π x)] (l : list δ) :
theorem measurable_tprod_elim {δ : Type u_4} {π : δ → Type u_7} [Π (x : δ), measurable_space (π x)] [decidable_eq δ] {l : list δ} {i : δ} (hi : i l) :
measurable (λ (v : l), v.elim hi)
theorem measurable_tprod_elim' {δ : Type u_4} {π : δ → Type u_7} [Π (x : δ), measurable_space (π x)] [decidable_eq δ] {l : list δ} (h : ∀ (i : δ), i l) :
theorem measurable_set.tprod {δ : Type u_4} {π : δ → Type u_7} [Π (x : δ), measurable_space (π x)] (l : list δ) {s : Π (i : δ), set (π i)} (hs : ∀ (i : δ), measurable_set (s i)) :
@[protected, instance]
def sum.measurable_space {α : Type u_1} {β : Type u_2} [m₁ : measurable_space α] [m₂ : measurable_space β] :
Equations
@[measurability]
theorem measurable_inl {α : Type u_1} {β : Type u_2}  :
@[measurability]
theorem measurable_inr {α : Type u_1} {β : Type u_2}  :
theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α β → γ} (hl : measurable (f sum.inl)) (hr : measurable (f sum.inr)) :
@[measurability]
theorem measurable.sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {f : α → γ} {g : β → γ} (hf : measurable f) (hg : measurable g) :
theorem measurable_set.inl_image {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set α} (hs : measurable_set s) :
theorem measurable_set_inr_image {α : Type u_1} {β : Type u_2} {m : measurable_space α} {mβ : measurable_space β} {s : set β} (hs : measurable_set s) :
theorem measurable_set_range_inl {α : Type u_1} {β : Type u_2} {mβ : measurable_space β}  :
theorem measurable_set_range_inr {α : Type u_1} {β : Type u_2} {mβ : measurable_space β}  :
@[protected, instance]
def sigma.measurable_space {α : Type u_1} {β : α → Type u_2} [m : Π (a : α), measurable_space (β a)] :
Equations
structure measurable_embedding {α : Type u_7} {β : Type u_8} (f : α → β) :
Prop
• injective :
• measurable :
• measurable_set_image' : ∀ ⦃s : set α⦄, measurable_set (f '' s)

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 : range f → α`”, see `measurable_embedding.measurable_range_splitting`, `measurable_embedding.of_measurable_inverse_range`, and `measurable_embedding.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 `measurable_embedding.equiv_range`; the other one follows from `measurable_equiv.measurable_embedding`, `measurable_embedding.subtype_coe`, and `measurable_embedding.comp`.

theorem measurable_embedding.measurable_set_image {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) {s : set α} :
theorem measurable_embedding.id {α : Type u_1} {mα : measurable_space α} :
theorem measurable_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {f : α → β} {g : β → γ} (hg : measurable_embedding g) (hf : measurable_embedding f) :
theorem measurable_embedding.subtype_coe {α : Type u_1} {mα : measurable_space α} {s : set α} (hs : measurable_set s) :
theorem measurable_embedding.measurable_set_range {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) :
theorem measurable_embedding.measurable_set_preimage {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) {s : set β} :
theorem measurable_embedding.measurable_range_splitting {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) :
theorem measurable_embedding.measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) {g : α → γ} {g' : β → γ} (hg : measurable g) (hg' : measurable g') :
theorem measurable_embedding.exists_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {f : α → β} (hf : measurable_embedding f) {g : α → γ} (hg : measurable g) (hne : β → ) :
∃ (g' : β → γ), g' f = g
theorem measurable_embedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {f : α → β} {g : β → γ} (hg : measurable_embedding g) :
theorem measurable_set.exists_measurable_proj {α : Type u_1} {m : measurable_space α} {s : set α} (hs : measurable_set s) (hne : s.nonempty) :
∃ (f : α → s), ∀ (x : s), f x = x
structure measurable_equiv (α : Type u_7) (β : Type u_8)  :
Type (max u_7 u_8)

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

Instances for `measurable_equiv`
@[protected, instance]
def measurable_equiv.has_coe_to_fun (α : Type u_1) (β : Type u_2)  :
has_coe_to_fun ≃ᵐ β) (λ (_x : α ≃ᵐ β), α → β)
Equations
@[simp]
theorem measurable_equiv.coe_to_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[protected, measurability]
theorem measurable_equiv.measurable {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[simp]
theorem measurable_equiv.coe_mk {α : Type u_1} {β : Type u_2} (e : α β) (h1 : measurable e) (h2 : measurable (e.symm)) :
def measurable_equiv.refl (α : Type u_1)  :
α ≃ᵐ α

Any measurable space is equivalent to itself.

Equations
@[protected, instance]
def measurable_equiv.inhabited {α : Type u_1}  :
Equations
def measurable_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
α ≃ᵐ γ

The composition of equivalences between measurable spaces.

Equations
def measurable_equiv.symm {α : Type u_1} {β : Type u_2} (ab : α ≃ᵐ β) :
β ≃ᵐ α

The inverse of an equivalence between measurable spaces.

Equations
@[simp]
theorem measurable_equiv.coe_to_equiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
def measurable_equiv.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
def measurable_equiv.simps.symm_apply {α : Type u_1} {β : Type u_2} (h : α ≃ᵐ β) :
β → α
Equations
theorem measurable_equiv.to_equiv_injective {α : Type u_1} {β : Type u_2}  :
@[ext]
theorem measurable_equiv.ext {α : Type u_1} {β : Type u_2} {e₁ e₂ : α ≃ᵐ β} (h : e₁ = e₂) :
e₁ = e₂
@[simp]
theorem measurable_equiv.symm_mk {α : Type u_1} {β : Type u_2} (e : α β) (h1 : measurable e) (h2 : measurable (e.symm)) :
@[simp]
theorem measurable_equiv.refl_to_equiv (α : Type u_1)  :
@[simp]
theorem measurable_equiv.trans_to_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :
@[simp]
theorem measurable_equiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) (ᾰ : α) :
(ab.trans bc) = bc (ab ᾰ)
@[simp]
theorem measurable_equiv.refl_apply (α : Type u_1) (a : α) :
= a
@[simp]
theorem measurable_equiv.symm_refl (α : Type u_1)  :
@[simp]
theorem measurable_equiv.symm_comp_self {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[simp]
theorem measurable_equiv.self_comp_symm {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[simp]
theorem measurable_equiv.apply_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) (y : β) :
e ((e.symm) y) = y
@[simp]
theorem measurable_equiv.symm_apply_apply {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) (x : α) :
(e.symm) (e x) = x
@[simp]
theorem measurable_equiv.symm_trans_self {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[simp]
theorem measurable_equiv.self_trans_symm {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[protected]
theorem measurable_equiv.surjective {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[protected]
theorem measurable_equiv.bijective {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[protected]
theorem measurable_equiv.injective {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
@[simp]
theorem measurable_equiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) (s : set β) :
theorem measurable_equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) (s : set α) :
e '' s = (e.symm) ⁻¹' s
@[simp]
theorem measurable_equiv.measurable_set_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) {s : set β} :
@[simp]
theorem measurable_equiv.measurable_set_image {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) {s : set α} :
@[protected]
theorem measurable_equiv.measurable_embedding {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :

A measurable equivalence is a measurable embedding.

@[protected]
def measurable_equiv.cast {α β : Type u_1} [i₁ : measurable_space α] [i₂ : measurable_space β] (h : α = β) (hi : i₁ == i₂) :
α ≃ᵐ β

Equal measurable spaces are equivalent.

Equations
@[protected]
theorem measurable_equiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} (e : α ≃ᵐ β) :
def measurable_equiv.of_unique_of_unique (α : Type u_1) (β : Type u_2) [unique α] [unique β] :
α ≃ᵐ β

Any two types with unique elements are measurably equivalent.

Equations
def measurable_equiv.prod_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
α × γ ≃ᵐ β × δ

Products of equivalent measurable spaces are equivalent.

Equations
def measurable_equiv.prod_comm {α : Type u_1} {β : Type u_2}  :
α × β ≃ᵐ β × α

Products of measurable spaces are symmetric.

Equations
def measurable_equiv.prod_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3}  :
× β) × γ ≃ᵐ α × β × γ

Products of measurable spaces are associative.

Equations
def measurable_equiv.sum_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :
α γ ≃ᵐ β δ

Sums of measurable spaces are symmetric.

Equations
def measurable_equiv.set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

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

Equations
def measurable_equiv.set.univ (α : Type u_1)  :

`univ α ≃ α` as measurable spaces.

Equations
def measurable_equiv.set.singleton {α : Type u_1} (a : α) :

`{a} ≃ unit` as measurable spaces.

Equations
noncomputable def measurable_equiv.set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (hf : function.injective f) (hfm : measurable f) (hfi : ∀ (s : set α), measurable_set (f '' s)) :

A set is equivalent to its image under a function `f` as measurable spaces, if `f` is an injective measurable function that sends measurable sets to measurable sets.

Equations
noncomputable def measurable_equiv.set.range {α : Type u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (hfm : measurable f) (hfi : ∀ (s : set α), measurable_set (f '' s)) :

The domain of `f` is equivalent to its range as measurable spaces, if `f` is an injective measurable function that sends measurable sets to measurable sets.

Equations
• hfm hfi = hfm hfi).trans _))
def measurable_equiv.set.range_inl {α : Type u_1} {β : Type u_2}  :

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

Equations
def measurable_equiv.set.range_inr {α : Type u_1} {β : Type u_2}  :

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

Equations
def measurable_equiv.sum_prod_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3)  :
β) × γ ≃ᵐ α × γ β × γ

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

Equations
def measurable_equiv.prod_sum_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3)  :
α × γ) ≃ᵐ α × β α × γ

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

Equations
def measurable_equiv.sum_prod_sum (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4)  :
β) × δ) ≃ᵐ × γ α × δ) β × γ β × δ

Products distribute over sums as measurable spaces.

Equations
def measurable_equiv.Pi_congr_right {δ' : Type u_5} {π : δ' → Type u_7} {π' : δ' → Type u_8} [Π (x : δ'), measurable_space (π x)] [Π (x : δ'), measurable_space (π' 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
@[simp]
theorem measurable_equiv.pi_measurable_equiv_tprod_apply {δ' : Type u_5} {π : δ' → Type u_7} [Π (x : δ'), measurable_space (π x)] [decidable_eq δ'] {l : list δ'} (hnd : l.nodup) (h : ∀ (i : δ'), i l) :
def measurable_equiv.pi_measurable_equiv_tprod {δ' : Type u_5} {π : δ' → Type u_7} [Π (x : δ'), measurable_space (π x)] [decidable_eq δ'] {l : list δ'} (hnd : l.nodup) (h : ∀ (i : δ'), i l) :
(Π (i : δ'), π i) ≃ᵐ l

Pi-types are measurably equivalent to iterated products.

Equations
@[simp]
theorem measurable_equiv.pi_measurable_equiv_tprod_to_equiv {δ' : Type u_5} {π : δ' → Type u_7} [Π (x : δ'), measurable_space (π x)] [decidable_eq δ'] {l : list δ'} (hnd : l.nodup) (h : ∀ (i : δ'), i l) :
@[simp]
theorem measurable_equiv.pi_measurable_equiv_tprod_symm_apply {δ' : Type u_5} {π : δ' → Type u_7} [Π (x : δ'), measurable_space (π x)] [decidable_eq δ'] {l : list δ'} (hnd : l.nodup) (h : ∀ (i : δ'), i l) :
def measurable_equiv.fun_unique (α : Type u_1) (β : Type u_2) [unique α]  :
(α → β) ≃ᵐ β

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

Equations
@[simp]
theorem measurable_equiv.fun_unique_to_equiv (α : Type u_1) (β : Type u_2) [unique α]  :
@[simp]
theorem measurable_equiv.fun_unique_apply (α : Type u_1) (β : Type u_2) [unique α]  :
@[simp]
theorem measurable_equiv.fun_unique_symm_apply (α : Type u_1) (β : Type u_2) [unique α]  :
.symm) = λ (x : β) (b : α), x
@[simp]
theorem measurable_equiv.pi_fin_two_symm_apply (α : fin 2Type u_1) [Π (i : fin 2), measurable_space (α i)] :
= λ (p : α 0 × α 1),
@[simp]
theorem measurable_equiv.pi_fin_two_apply (α : fin 2Type u_1) [Π (i : fin 2), measurable_space (α i)] :
= λ (f : Π (i : fin 2), α i), (f 0, f 1)
@[simp]
theorem measurable_equiv.pi_fin_two_to_equiv (α : fin 2Type u_1) [Π (i : fin 2), measurable_space (α i)] :
def measurable_equiv.pi_fin_two (α : fin 2Type u_1) [Π (i : fin 2), measurable_space (α i)] :
(Π (i : fin 2), α i) ≃ᵐ α 0 × α 1

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

Equations
@[simp]
theorem measurable_equiv.fin_two_arrow_apply {α : Type u_1}  :
measurable_equiv.fin_two_arrow = λ (f : fin 2 → α), (f 0, f 1)
@[simp]
theorem measurable_equiv.fin_two_arrow_to_equiv_apply {α : Type u_1}  :
(measurable_equiv.fin_two_arrow.to_equiv) = λ (f : fin 2 → α), (f 0, f 1)
@[simp]
def measurable_equiv.fin_two_arrow {α : Type u_1}  :
(fin 2 → α) ≃ᵐ α × α

The space `fin 2 → α` is measurably equivalent to `α × α`.

Equations
def measurable_equiv.pi_fin_succ_above_equiv {n : } (α : fin (n + 1)Type u_1) [Π (i : fin (n + 1)), measurable_space (α i)] (i : fin (n + 1)) :
(Π (j : fin (n + 1)), α j) ≃ᵐ α i × Π (j : fin n), α ((i.succ_above) j)

Measurable equivalence between `Π j : fin (n + 1), α j` and `α i × Π j : fin n, α (fin.succ_above i j)`.

Equations
@[simp]
theorem measurable_equiv.pi_fin_succ_above_equiv_apply {n : } (α : fin (n + 1)Type u_1) [Π (i : fin (n + 1)), measurable_space (α i)] (i : fin (n + 1)) :
= λ (f : Π (j : fin (n + 1)), α j), (f i, λ (j : fin n), f ((i.succ_above) j))
@[simp]
theorem measurable_equiv.pi_fin_succ_above_equiv_to_equiv {n : } (α : fin (n + 1)Type u_1) [Π (i : fin (n + 1)), measurable_space (α i)] (i : fin (n + 1)) :
@[simp]
theorem measurable_equiv.pi_fin_succ_above_equiv_symm_apply {n : } (α : fin (n + 1)Type u_1) [Π (i : fin (n + 1)), measurable_space (α i)] (i : fin (n + 1)) :
= λ (f : α i × Π (j : fin n), α ((i.succ_above) j)), i.insert_nth f.fst f.snd
def measurable_equiv.pi_equiv_pi_subtype_prod {δ' : Type u_5} (π : δ' → Type u_7) [Π (x : δ'), measurable_space (π x)] (p : δ' → Prop)  :
(Π (i : δ'), π i) ≃ᵐ (Π (i : subtype p), π 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.pi_equiv_pi_subtype_prod`.

Equations
@[simp]
theorem measurable_equiv.pi_equiv_pi_subtype_prod_symm_apply {δ' : Type u_5} (π : δ' → Type u_7) [Π (x : δ'), measurable_space (π x)] (p : δ' → Prop)  :
= λ (f : (Π (i : subtype p), π i) × Π (i : {x // ¬p x}), π i) (x : δ'), dite (p x) (λ (h : p x), f.fst x, h⟩) (λ (h : ¬p x), f.snd x, h⟩)
@[simp]
theorem measurable_equiv.pi_equiv_pi_subtype_prod_to_equiv {δ' : Type u_5} (π : δ' → Type u_7) [Π (x : δ'), measurable_space (π x)] (p : δ' → Prop)  :
@[simp]
theorem measurable_equiv.pi_equiv_pi_subtype_prod_apply {δ' : Type u_5} (π : δ' → Type u_7) [Π (x : δ'), measurable_space (π x)] (p : δ' → Prop)  :
= λ (f : Π (i : δ'), π i), (λ (x : subtype p), f x, λ (x : {x // ¬p x}), f x)
noncomputable def measurable_embedding.equiv_range {α : Type u_1} {β : Type u_2} (f : α → β) (hf : measurable_embedding f) :

A measurable embedding defines a measurable equivalence between its domain and its range.

Equations
theorem measurable_embedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} {f : α → β} {g : (set.range f) → α} (hf₁ : measurable f) (hf₂ : measurable_set (set.range f)) (hg : measurable g) (H : ) :
theorem measurable_embedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} (hf₁ : measurable f) (hf₂ : measurable_set (set.range f)) (hg : measurable g) (H : f) :
@[class]
structure filter.is_measurably_generated {α : Type u_1} (f : filter α) :
Prop
• exists_measurable_subset : ∀ ⦃s : set α⦄, s f(∃ (t : set α) (H : t f), t s)

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

Instances of this typeclass
@[protected, instance]
def filter.is_measurably_generated_bot {α : Type u_1}  :
@[protected, instance]
def filter.is_measurably_generated_top {α : Type u_1}  :
theorem filter.eventually.exists_measurable_mem {α : Type u_1} {f : filter α} {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) :
∃ (s : set α) (H : s f), ∀ (x : α), x sp x
theorem filter.eventually.exists_measurable_mem_of_small_sets {α : Type u_1} {f : filter α} {p : set α → Prop} (h : ∀ᶠ (s : set α) in f.small_sets, p s) :
∃ (s : set α) (H : s f), p s
@[protected, instance]
def filter.inf_is_measurably_generated {α : Type u_1} (f g : filter α)  :
theorem filter.principal_is_measurably_generated_iff {α : Type u_1} {s : set α} :
theorem measurable_set.principal_is_measurably_generated {α : Type u_1} {s : set α} :

Alias of the reverse direction of `filter.principal_is_measurably_generated_iff`.

@[protected, instance]
def filter.infi_is_measurably_generated {α : Type u_1} {ι : Sort u_6} {f : ι → } [∀ (i : ι), (f i).is_measurably_generated] :
(⨅ (i : ι), f i).is_measurably_generated
def is_countably_spanning {α : Type u_1} (C : set (set α)) :
Prop

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 `generate_from_prod_eq`.

Equations

### Typeclasses on `subtype measurable_set`#

@[protected, instance]
def measurable_set.subtype.has_mem {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.mem_coe {α : Type u_1} (a : α)  :
a s a s
@[protected, instance]
def measurable_set.subtype.has_emptyc {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_empty {α : Type u_1}  :
@[protected, instance]
def measurable_set.subtype.has_insert {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_insert {α : Type u_1} (a : α)  :
s) =
@[protected, instance]
def measurable_set.subtype.has_compl {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_compl {α : Type u_1}  :
@[protected, instance]
def measurable_set.subtype.has_union {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_union {α : Type u_1} (s t : subtype measurable_set) :
(s t) = s t
@[protected, instance]
def measurable_set.subtype.has_inter {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_inter {α : Type u_1} (s t : subtype measurable_set) :
(s t) = s t
@[protected, instance]
def measurable_set.subtype.has_sdiff {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_sdiff {α : Type u_1} (s t : subtype measurable_set) :
(s \ t) = s \ t
@[protected, instance]
def measurable_set.subtype.has_bot {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_bot {α : Type u_1}  :
@[protected, instance]
def measurable_set.subtype.has_top {α : Type u_1}  :
Equations
@[simp]
theorem measurable_set.coe_top {α : Type u_1}  :
@[protected, instance]
def measurable_set.subtype.partial_order {α : Type u_1}  :
Equations
@[protected, instance]
def measurable_set.subtype.distrib_lattice {α : Type u_1}  :
Equations
@[protected, instance]
def measurable_set.subtype.bounded_order {α : Type u_1}  :
Equations
@[protected, instance]
def measurable_set.subtype.boolean_algebra {α : Type u_1}  :
Equations