Documentation

Mathlib.MeasureTheory.MeasurableSpace.Basic

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 β.

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.

Implementation notes #

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

References #

Tags #

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

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

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
Instances For
    theorem MeasurableSpace.map_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : αβ} {s : Set β} :
    @[simp]
    @[simp]
    theorem MeasurableSpace.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : αβ} {g : βγ} :
    def MeasurableSpace.comap {α : Type u_1} {β : Type u_2} (f : αβ) (m : MeasurableSpace β) :

    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 : MeasurableSpace β) (f : αβ) :
      @[simp]
      @[simp]
      theorem MeasurableSpace.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : βα} {g : γβ} :
      theorem MeasurableSpace.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : αβ} :
      theorem MeasurableSpace.map_mono {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {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₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {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₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {g : βα} :
      @[simp]
      theorem MeasurableSpace.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : βα} {m : ιMeasurableSpace α} :
      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₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {f : αβ} :
      @[simp]
      theorem MeasurableSpace.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : αβ} {m : ιMeasurableSpace α} :
      MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)
      theorem MeasurableSpace.comap_map_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : αβ} :
      theorem MeasurableSpace.le_map_comap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : βα} :
      @[simp]
      theorem MeasurableSpace.map_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} (b : β) :
      MeasurableSpace.map (fun (_a : α) => b) m =
      @[simp]
      theorem MeasurableSpace.comap_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (b : β) :
      MeasurableSpace.comap (fun (_a : α) => b) m =
      theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :
      theorem Measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : αβ} :

      Alias of the reverse direction of measurable_iff_le_map.

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

      Alias of the forward direction of measurable_iff_le_map.

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

      Alias of the reverse direction of measurable_iff_comap_le.

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

      Alias of the forward direction of measurable_iff_comap_le.

      theorem comap_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (f : αβ) :
      theorem Measurable.mono {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {ma' : MeasurableSpace α} {mb : MeasurableSpace β} {mb' : MeasurableSpace β} {f : αβ} (hf : Measurable f) (ha : ma ma') (hb : mb' mb) :
      theorem measurable_id'' {α : Type u_1} {m : MeasurableSpace α} {mα : MeasurableSpace α} (hm : m ) :
      theorem measurable_from_top {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : αβ} :
      theorem measurable_generateFrom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set (Set β)} {f : αβ} (h : ts, MeasurableSet (f ⁻¹' t)) :
      theorem Subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : αβ} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton α] :
      theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton β] (f : αβ) :
      theorem measurable_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Zero α] :
      theorem measurable_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [One α] :
      theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty α] (f : αβ) :
      theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty β] (f : αβ) :
      theorem measurable_const' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {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} [MeasurableSpace α] [MeasurableSpace β] [NatCast α] (n : ) :
      theorem measurable_intCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IntCast α] (n : ) :
      theorem measurable_of_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : αβ) :
      theorem measurable_of_finite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] (f : αβ) :
      theorem Measurable.iterate {α : Type u_1} {m : MeasurableSpace α} {f : αα} (hf : Measurable f) (n : ) :
      theorem measurableSet_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (hf : Measurable f) (ht : MeasurableSet t) :
      theorem MeasurableSet.preimage {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (ht : MeasurableSet t) (hf : Measurable f) :
      theorem Measurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
      ∀ {x : DecidablePred fun (x : α) => x s}, MeasurableSet sMeasurable fMeasurable gMeasurable (s.piecewise f g)
      theorem Measurable.ite {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : αProp} :
      ∀ {x : DecidablePred p}, MeasurableSet {a : α | p a}Measurable fMeasurable gMeasurable 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 : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] (hf : Measurable f) (hs : MeasurableSet s) :
      Measurable (s.indicator f)
      theorem measurable_indicator_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] :
      Measurable (s.indicator fun (x : α) => b) MeasurableSet s

      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 : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (hf : Measurable f) :
      theorem measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [One β] [MeasurableSingletonClass β] (hf : Measurable f) :
      theorem Measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] (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.

      theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : βα} (h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})) :
      theorem measurable_to_countable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : βα} (h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})) :
      theorem measurable_unit {α : Type u_1} [MeasurableSpace α] (f : Unitα) :
      Equations
      theorem measurable_down {α : Type u_1} [MeasurableSpace α] :
      Measurable ULift.down
      theorem measurable_up {α : Type u_1} [MeasurableSpace α] :
      Measurable ULift.up
      @[simp]
      theorem measurableSet_preimage_down {α : Type u_1} [MeasurableSpace α] {s : Set α} :
      theorem measurable_from_nat {α : Type u_1} [MeasurableSpace α] {f : α} :
      theorem measurable_to_nat {α : Type u_1} [MeasurableSpace α] {f : α} :
      (∀ (y : α), MeasurableSet (f ⁻¹' {f y}))Measurable f
      theorem measurable_to_bool {α : Type u_1} [MeasurableSpace α] {f : αBool} (h : MeasurableSet (f ⁻¹' {true})) :
      theorem measurable_to_prop {α : Type u_1} [MeasurableSpace α] {f : αProp} (h : MeasurableSet (f ⁻¹' {True})) :
      theorem measurable_findGreatest' {α : Type u_1} [MeasurableSpace α] {p : αProp} [(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} [MeasurableSpace α] {p : αProp} [(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} [MeasurableSpace α] {p : αProp} [(x : α) → DecidablePred (p x)] (hp : ∀ (x : α), ∃ (N : ), p x N) (hm : ∀ (k : ), MeasurableSet {x : α | p x k}) :
      Measurable fun (x : α) => Nat.find
      instance Quot.instMeasurableSpace {α : Type u_6} {r : ααProp} [m : MeasurableSpace α] :
      Equations
      Equations
      Equations
      Equations
      theorem measurableSet_quotient {α : Type u_1} [MeasurableSpace α] {s : Setoid α} {t : Set (Quotient s)} :
      theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {s : Setoid α} {f : Quotient sβ} :
      Measurable f Measurable (f Quotient.mk'')
      theorem measurable_quotient_mk' {α : Type u_1} [MeasurableSpace α] [s : Setoid α] :
      Measurable Quotient.mk'
      theorem measurable_quotient_mk'' {α : Type u_1} [MeasurableSpace α] {s : Setoid α} :
      Measurable Quotient.mk''
      theorem measurable_quot_mk {α : Type u_1} [MeasurableSpace α] {r : ααProp} :
      theorem QuotientAddGroup.measurable_coe {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} :
      Measurable QuotientAddGroup.mk
      theorem QuotientGroup.measurable_coe {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} :
      Measurable QuotientGroup.mk
      theorem QuotientAddGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} {f : G Sα} :
      Measurable f Measurable (f QuotientAddGroup.mk)
      theorem QuotientGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} {f : G Sα} :
      Measurable f Measurable (f QuotientGroup.mk)
      instance Subtype.instMeasurableSpace {α : Type u_6} {p : αProp} [m : MeasurableSpace α] :
      Equations
      theorem measurable_subtype_coe {α : Type u_1} [MeasurableSpace α] {p : αProp} :
      Measurable Subtype.val
      theorem MeasurableSet.of_subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set s} (h : MeasurableSet (Subtype.val '' t)) :
      theorem MeasurableSet.subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set s} (hs : MeasurableSet s) :
      MeasurableSet tMeasurableSet (Subtype.val '' t)
      theorem Measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αSubtype p} (hf : Measurable f) :
      Measurable fun (a : α) => (f a)
      theorem Measurable.subtype_val {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αSubtype p} (hf : Measurable f) :
      Measurable fun (a : α) => (f a)

      Alias of Measurable.subtype_coe.

      theorem Measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : βProp} {f : αβ} (hf : Measurable f) {h : ∀ (x : α), p (f x)} :
      Measurable fun (x : α) => f x,
      theorem Measurable.rangeFactorization {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (hf : Measurable f) :
      theorem Measurable.subtype_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} {p : αProp} {q : βProp} (hf : Measurable f) (hpq : ∀ (x : α), p xq (f x)) :
      theorem measurable_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) :
      theorem MeasurableSet.image_inclusion' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : MeasurableSet u) :
      theorem MeasurableSet.image_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s t) {u : Set s} (hs : MeasurableSet s) (hu : MeasurableSet u) :
      theorem MeasurableSet.of_union_cover {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (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 : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} (s : Set α) (t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (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 : MeasurableSpace α} {mβ : MeasurableSpace β} {f : αβ} {s : Set α} (hs : MeasurableSet s) (h₁ : Measurable (s.restrict f)) (h₂ : Measurable (s.restrict f)) :
      theorem Measurable.dite {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [(x : α) → Decidable (x s)] {f : sβ} (hf : Measurable f) {g : sβ} (hg : Measurable g) (hs : MeasurableSet s) :
      Measurable fun (x : α) => if hx : x s then f x, hx else g x, hx
      theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {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 : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : αβ} (a : α) (hf : Measurable ({x : α | x a}.restrict f)) :
      def measurableAtom {β : Type u_2} [MeasurableSpace β] (x : β) :
      Set β

      The measurable atom of x is the intersection of all the measurable sets countaining x. It is measurable when the space is countable (or more generally when the measurable space is countably generated).

      Equations
      Instances For
        @[simp]
        theorem mem_measurableAtom_self {β : Type u_2} [MeasurableSpace β] (x : β) :
        theorem mem_of_mem_measurableAtom {β : Type u_2} [MeasurableSpace β] {x : β} {y : β} (h : y measurableAtom x) {s : Set β} (hs : MeasurableSet s) (hxs : x s) :
        y s
        theorem measurableAtom_subset {β : Type u_2} [MeasurableSpace β] {s : Set β} {x : β} (hs : MeasurableSet s) (hx : x s) :
        def MeasurableSpace.prod {α : Type u_6} {β : Type u_7} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β) :

        A MeasurableSpace structure on the product of two measurable spaces.

        Equations
        Instances For
          instance Prod.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
          Equations
          • Prod.instMeasurableSpace = m₁.prod m₂
          theorem measurable_fst {α : Type u_1} {β : Type u_2} :
          ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst
          theorem measurable_snd {α : Type u_1} {β : Type u_2} :
          ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd
          theorem Measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf : Measurable f) :
          Measurable fun (a : α) => (f a).1
          theorem Measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf : Measurable f) :
          Measurable fun (a : α) => (f a).2
          theorem Measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} (hf₁ : Measurable fun (a : α) => (f a).1) (hf₂ : Measurable fun (a : α) => (f a).2) :
          theorem Measurable.prod_mk {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} :
          ∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : αβ} {g : αγ}, Measurable fMeasurable gMeasurable fun (a : α) => (f a, g a)
          theorem Measurable.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace δ] {f : αβ} {g : γδ} (hf : Measurable f) (hg : Measurable g) :
          theorem measurable_prod_mk_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α} :
          theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β} :
          Measurable fun (x : α) => (x, y)
          theorem Measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβγ} (hf : Measurable (Function.uncurry f)) {x : α} :
          theorem Measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβγ} (hf : Measurable (Function.uncurry f)) {y : β} :
          Measurable fun (x : α) => f x y
          theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : αβ × γ} :
          Measurable f (Measurable fun (a : α) => (f a).1) Measurable fun (a : α) => (f a).2
          theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
          Measurable Prod.swap
          theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
          ∀ {x : MeasurableSpace γ} {f : α × βγ}, Measurable (f Prod.swap) Measurable f
          theorem MeasurableSet.prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :
          theorem measurableSet_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (h : (s ×ˢ t).Nonempty) :
          theorem measurableSet_prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} :
          theorem measurableSet_swap_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α × β)} :
          theorem measurable_from_prod_countable' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable β] :
          ∀ {x : MeasurableSpace γ} {f : α × βγ}, (∀ (y : β), Measurable fun (x : α) => f (x, y))(∀ (y y' : β) (x : α), y' measurableAtom yf (x, y') = f (x, y))Measurable f
          theorem measurable_from_prod_countable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable β] [MeasurableSingletonClass β] :
          ∀ {x : MeasurableSpace γ} {f : α × βγ}, (∀ (y : β), Measurable fun (x : α) => f (x, y))Measurable f
          theorem Measurable.find {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} :
          ∀ {x : MeasurableSpace α} {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 ) 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 : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] {t : ιSet α} {f : (i : ι) → (t i)β} (htf : ∀ (i j : ι) (x : α) (hxi : x t i) (hxj : x t j), f i x, hxi = f j x, 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 : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (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 x, hxi = f j x, 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 : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [Countable ι] [Nonempty ι] (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 : αβ), Measurable 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 (α → β)].

          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} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {g : α(a : δ) → π a} :
          Measurable g ∀ (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} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {a : δ} {g : α(a : δ) → π a} (hg : Measurable g) :
          Measurable fun (x : α) => g x a
          theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {π : δType u_6} [MeasurableSpace α] [(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 : δ} [DecidableEq δ] :
          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} [Unique δ] [(i : δ) → MeasurableSpace (π i)] :
          Measurable uniqueElim
          theorem measurable_updateFinset {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [DecidableEq δ] {s : Finset δ} {x : (i : δ) → π i} :
          theorem measurable_update {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [DecidableEq δ] :

          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 : δ} [DecidableEq δ] {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 .mp
          theorem Measurable.eq_mp {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] {β : Type u_7} [MeasurableSpace β] {i : δ} {i' : δ} (h : i = i') {f : βπ i} (hf : Measurable f) :
          Measurable fun (x : β) => .mp (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 : s.Countable) (ht : is, MeasurableSet (t i)) :
          MeasurableSet (s.pi t)
          theorem MeasurableSet.univ_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] {t : (i : δ) → Set (π i)} (ht : ∀ (i : δ), MeasurableSet (t i)) :
          MeasurableSet (Set.univ.pi t)
          theorem measurableSet_pi_of_nonempty {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : s.Countable) (h : (s.pi t).Nonempty) :
          MeasurableSet (s.pi t) is, MeasurableSet (t i)
          theorem measurableSet_pi {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : s.Countable) :
          MeasurableSet (s.pi t) (is, MeasurableSet (t i)) s.pi t =
          instance Pi.instMeasurableSingletonClass {δ : Type u_4} {π : δType u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] [∀ (a : δ), MeasurableSingletonClass (π a)] :
          MeasurableSingletonClass ((a : δ) → π a)
          Equations
          • =
          theorem measurable_piEquivPiSubtypeProd_symm {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [DecidablePred p] :
          theorem measurable_piEquivPiSubtypeProd {δ : Type u_4} (π : δType u_6) [(a : δ) → MeasurableSpace (π a)] (p : δProp) [DecidablePred p] :
          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)] [DecidableEq δ] {l : List δ} {i : δ} (hi : i l) :
          Measurable fun (v : List.TProd π l) => v.elim hi
          theorem measurable_tProd_elim' {δ : Type u_4} {π : δType u_6} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] {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₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :
          Equations
          theorem measurable_inl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
          Measurable Sum.inl
          theorem measurable_inr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :
          Measurable Sum.inr
          theorem measurableSet_sum_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α β)} :
          theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
          ∀ {x : MeasurableSpace γ} {f : α βγ}, Measurable (f Sum.inl)Measurable (f Sum.inr)Measurable f
          theorem Measurable.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
          ∀ {x : MeasurableSpace γ} {f : αγ} {g : βγ}, Measurable fMeasurable gMeasurable (Sum.elim f g)
          theorem Measurable.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :
          ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace δ} {f : αβ} {g : γδ}, Measurable fMeasurable gMeasurable (Sum.map f g)
          @[simp]
          theorem measurableSet_inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
          theorem MeasurableSet.inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :
          MeasurableSet sMeasurableSet (Sum.inl '' s)

          Alias of the reverse direction of measurableSet_inl_image.

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

          Alias of the reverse direction of measurableSet_inr_image.

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

          Alias of the reverse direction of measurableSet_setOf.

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

          Alias of the reverse direction of measurable_mem.

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

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

          Equations
          • Set.instMeasurableSpace = id inferInstance
          theorem measurable_set_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {g : βSet α} :
          Measurable g ∀ (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]

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

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

          Instances
            theorem Filter.IsMeasurablyGenerated.exists_measurable_subset {α : Type u_1} [MeasurableSpace α] {f : Filter α} [self : f.IsMeasurablyGenerated] ⦃s : Set α :
            s ftf, MeasurableSet t t s
            instance Filter.isMeasurablyGenerated_bot {α : Type u_1} [MeasurableSpace α] :
            .IsMeasurablyGenerated
            Equations
            • =
            instance Filter.isMeasurablyGenerated_top {α : Type u_1} [MeasurableSpace α] :
            .IsMeasurablyGenerated
            Equations
            • =
            theorem Filter.Eventually.exists_measurable_mem {α : Type u_1} [MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : αProp} (h : ∀ᶠ (x : α) in f, p x) :
            sf, MeasurableSet s xs, p x
            theorem Filter.Eventually.exists_measurable_mem_of_smallSets {α : Type u_1} [MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : Set αProp} (h : ∀ᶠ (s : Set α) in f.smallSets, p s) :
            sf, MeasurableSet s p s
            instance Filter.inf_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f : Filter α) (g : Filter α) [f.IsMeasurablyGenerated] [g.IsMeasurablyGenerated] :
            (f g).IsMeasurablyGenerated
            Equations
            • =
            theorem Filter.principal_isMeasurablyGenerated_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} :
            (Filter.principal s).IsMeasurablyGenerated MeasurableSet s
            theorem MeasurableSet.principal_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] {s : Set α} :
            MeasurableSet s(Filter.principal s).IsMeasurablyGenerated

            Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff.

            instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] {f : ιFilter α} [∀ (i : ι), (f i).IsMeasurablyGenerated] :
            (⨅ (i : ι), f i).IsMeasurablyGenerated
            Equations
            • =
            theorem measurableSet_tendsto {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
            ∀ {x : MeasurableSpace β} [inst : MeasurableSpace γ] [inst_1 : Countable δ] {l : Filter δ} [inst_2 : l.IsCountablyGenerated] (l' : Filter γ) [inst_3 : l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated] {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} [MeasurableSpace α] :
              Membership α (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instMembership = { mem := fun (a : α) (s : Subtype MeasurableSet) => a s }
              @[simp]
              theorem MeasurableSet.mem_coe {α : Type u_1} [MeasurableSpace α] (a : α) (s : Subtype MeasurableSet) :
              a s a s
              Equations
              • MeasurableSet.Subtype.instEmptyCollection = { emptyCollection := , }
              @[simp]
              theorem MeasurableSet.coe_empty {α : Type u_1} [MeasurableSpace α] :
              =
              Equations
              • MeasurableSet.Subtype.instInsert = { insert := fun (a : α) (s : Subtype MeasurableSet) => insert a s, }
              @[simp]
              theorem MeasurableSet.coe_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet) :
              (insert a s) = insert a s
              Equations
              • MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => {a}, }
              @[simp]
              theorem MeasurableSet.coe_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :
              {a} = {a}
              instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [MeasurableSpace α] :
              HasCompl (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instHasCompl = { compl := fun (x : Subtype MeasurableSet) => (x), }
              @[simp]
              theorem MeasurableSet.coe_compl {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) :
              s = (s)
              instance MeasurableSet.Subtype.instUnion {α : Type u_1} [MeasurableSpace α] :
              Union (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instUnion = { union := fun (x y : Subtype MeasurableSet) => x y, }
              @[simp]
              theorem MeasurableSet.coe_union {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
              (s t) = s t
              instance MeasurableSet.Subtype.instSup {α : Type u_1} [MeasurableSpace α] :
              Sup (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instSup = { sup := fun (x y : Subtype MeasurableSet) => x y }
              @[simp]
              theorem MeasurableSet.sup_eq_union {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :
              s t = s t
              instance MeasurableSet.Subtype.instInter {α : Type u_1} [MeasurableSpace α] :
              Inter (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instInter = { inter := fun (x y : Subtype MeasurableSet) => x y, }
              @[simp]
              theorem MeasurableSet.coe_inter {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
              (s t) = s t
              instance MeasurableSet.Subtype.instInf {α : Type u_1} [MeasurableSpace α] :
              Inf (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instInf = { inf := fun (x y : Subtype MeasurableSet) => x y }
              @[simp]
              theorem MeasurableSet.inf_eq_inter {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :
              s t = s t
              instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [MeasurableSpace α] :
              SDiff (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instSDiff = { sdiff := fun (x y : Subtype MeasurableSet) => x \ y, }
              noncomputable instance MeasurableSet.Subtype.instHImp {α : Type u_1} [MeasurableSpace α] :
              HImp (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instHImp = { himp := fun (x y : Subtype MeasurableSet) => x y, }
              @[simp]
              theorem MeasurableSet.coe_sdiff {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
              (s \ t) = s \ t
              @[simp]
              theorem MeasurableSet.coe_himp {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :
              (s t) = s t
              instance MeasurableSet.Subtype.instBot {α : Type u_1} [MeasurableSpace α] :
              Bot (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instBot = { bot := }
              @[simp]
              theorem MeasurableSet.coe_bot {α : Type u_1} [MeasurableSpace α] :
              =
              instance MeasurableSet.Subtype.instTop {α : Type u_1} [MeasurableSpace α] :
              Top (Subtype MeasurableSet)
              Equations
              • MeasurableSet.Subtype.instTop = { top := Set.univ, }
              @[simp]
              theorem MeasurableSet.coe_top {α : Type u_1} [MeasurableSpace α] :
              =
              noncomputable instance MeasurableSet.Subtype.instBooleanAlgebra {α : Type u_1} [MeasurableSpace α] :
              BooleanAlgebra (Subtype MeasurableSet)
              Equations
              theorem MeasurableSet.measurableSet_blimsup {α : Type u_1} [MeasurableSpace α] {s : Set α} {p : Prop} (h : ∀ (n : ), p nMeasurableSet (s n)) :
              MeasurableSet (Filter.blimsup s Filter.atTop p)
              theorem MeasurableSet.measurableSet_bliminf {α : Type u_1} [MeasurableSpace α] {s : Set α} {p : Prop} (h : ∀ (n : ), p nMeasurableSet (s n)) :
              MeasurableSet (Filter.bliminf s Filter.atTop p)
              theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
              MeasurableSet (Filter.limsup s Filter.atTop)
              theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : ∀ (n : ), MeasurableSet (s n)) :
              MeasurableSet (Filter.liminf s Filter.atTop)