theorem MeasureTheory.NoAtoms'.measure_comap_eq_subtype_coe {α : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) {t : Set ↑s} (ht : NullMeasurableSet t (Measure.comap Subtype.val μ)) : (Measure.comap Subtype.val μ) t = μ (Subtype.val '' t)

theorem MeasureTheory.NoAtoms'.subtype {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s : Set α} (hs : MeasurableSet s) : NoAtoms' (Measure.comap Subtype.val μ)

theorem MeasureTheory.NoAtoms'.exists_measurable_between {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s t : Set α} (hs : MeasurableSet s) (ht : NullMeasurableSet t μ) (h : s ⊆ t) (h' : μ s < μ t) : ∃ (u : Set α), MeasurableSet u ∧ s ⊆ u ∧ u ⊆ t ∧ μ s < μ u ∧ μ u < μ t

theorem MeasureTheory.NoAtoms'.exists_nullmeasurable_between {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (h : s ⊆ t) (h' : μ s < μ t) : ∃ (u : Set α), NullMeasurableSet u μ ∧ s ⊆ u ∧ u ⊆ t ∧ μ s < μ u ∧ μ u < μ t

@[simp]

theorem MeasureTheory.NoAtoms'.PFun.mem_graph'_iff {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} {b : β} : (a, b) ∈ f.graph' ↔ b ∈ f a

noncomputable def MeasureTheory.NoAtoms'.PFun.ofGraph' {α : Type u_1} {β : Type u_2} (r : SetRel α β) : α →. β

Constructs a partial function α →. β from its graph of type SetRel α β.

Equations

• MeasureTheory.NoAtoms'.PFun.ofGraph' r a = if h : ∃ (b : β), (a, b) ∈ r then Part.some h.choose else Part.none

theorem MeasureTheory.NoAtoms'.PFun.compare_of_mem_ofGraph' {α : Type u_1} {β : Type u_2} {r : SetRel α β} {a : α} {b : β} (hb : b ∈ ofGraph' r a) : (a, b) ∈ r

theorem MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_of_compare {α : Type u_1} {β : Type u_2} {r : SetRel α β} (h : ∀ (a : α) (b c : β), (a, b) ∈ r → (a, c) ∈ r → b = c) {a : α} {b : β} (hb : (a, b) ∈ r) : b ∈ ofGraph' r a

theorem MeasureTheory.NoAtoms'.PFun.mem_ofGraph'_iff_compare {α : Type u_1} {β : Type u_2} {r : SetRel α β} (h : ∀ (a : α) (b c : β), (a, b) ∈ r → (a, c) ∈ r → b = c) {a : α} {b : β} : b ∈ ofGraph' r a ↔ (a, b) ∈ r

theorem MeasureTheory.NoAtoms'.PFun.graph'_ofGraph' {α : Type u_1} {β : Type u_2} {r : SetRel α β} (h : ∀ (a : α) (b c : β), (a, b) ∈ r → (a, c) ∈ r → b = c) : (ofGraph' r).graph' = r

theorem MeasureTheory.NoAtoms'.PFun.graph_injective {α : Type u_1} {β : Type u_2} : Function.Injective PFun.graph

theorem MeasureTheory.NoAtoms'.PFun.graph'_injective {α : Type u_1} {β : Type u_2} : Function.Injective PFun.graph'

@[instance_reducible]

instance MeasureTheory.NoAtoms'.instPartialOrderPFun {α : Type u_1} {β : Type u_2} : PartialOrder (α →. β)

Equations

• MeasureTheory.NoAtoms'.instPartialOrderPFun = PartialOrder.lift PFun.graph' ⋯

theorem MeasureTheory.NoAtoms'.PFun.le_iff {α : Type u_1} {β : Type u_2} {f g : α →. β} : f ≤ g ↔ f.graph' ⊆ g.graph'

theorem MeasureTheory.NoAtoms'.PFun.le_iff' {α : Type u_1} {β : Type u_2} {f g : α →. β} : f ≤ g ↔ ∀ (a : α), ∀ b ∈ f a, b ∈ g a

theorem MeasureTheory.NoAtoms'.PFun.Dom_mono {α : Type u_1} {β : Type u_2} {f g : α →. β} (h : f ≤ g) : f.Dom ⊆ g.Dom

theorem MeasureTheory.NoAtoms'.PFun.fn_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} (ha : a ∈ f.Dom) : f.fn a ha ∈ f a

theorem MeasureTheory.NoAtoms'.PFun.fn_apply_eq_fn_apply_of_le {α : Type u_1} {β : Type u_2} {f g : α →. β} (h : f ≤ g) {a : α} (ha : a ∈ f.Dom) : f.fn a ha = g.fn a ⋯

theorem MeasureTheory.NoAtoms'.PFun.apply_eq_of_le {α : Type u_1} {β : Type u_2} {f g : α →. β} (h : f ≤ g) {a : α} (ha : a ∈ f.Dom) : f a = g a

@[instance_reducible]

noncomputable instance MeasureTheory.NoAtoms'.instSupSetPFun {α : Type u_1} {β : Type u_2} : SupSet (α →. β)

Equations

• MeasureTheory.NoAtoms'.instSupSetPFun = { sSup := fun (S : Set (α →. β)) => MeasureTheory.NoAtoms'.PFun.ofGraph' (sSup (PFun.graph' '' S)) }

theorem MeasureTheory.NoAtoms'.PFun.sSup_eq {α : Type u_1} {β : Type u_2} {fs : Set (α →. β)} : sSup fs = ofGraph' (⋃ a ∈ fs, a.graph')

theorem MeasureTheory.NoAtoms'.PFun.exists_mem_of_mem_sSup {α : Type u_1} {β : Type u_2} {fs : Set (α →. β)} {a : α} {b : β} (ha : b ∈ sSup fs a) : ∃ f ∈ fs, b ∈ f a

theorem MeasureTheory.NoAtoms'.PFun.le_sSup {α : Type u_1} {β : Type u_2} {fs : Set (α →. β)} (h : IsChain (fun (x1 x2 : α →. β) => x1 ≤ x2) fs) {f : α →. β} (hf : f ∈ fs) : f ≤ sSup fs

theorem MeasureTheory.NoAtoms'.PFun.mem_dom_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} {b : β} (h : b ∈ f a) : a ∈ f.Dom

theorem MeasureTheory.NoAtoms'.PFun.exists_fn_of_fn_sSup {α : Type u_1} {β : Type u_2} {fs : Set (α →. β)} (h : IsChain (fun (x1 x2 : α →. β) => x1 ≤ x2) fs) {a : α} (ha : a ∈ (sSup fs).Dom) : ∃ f ∈ fs, ∃ (haf : a ∈ f.Dom), (sSup fs).fn a ha = f.fn a haf

noncomputable def MeasureTheory.NoAtoms'.PFun.insert {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) (b : β) : α →. β

Gives the partial function sending a to b and agreeing with f otherwise.

Equations

• MeasureTheory.NoAtoms'.PFun.insert f a b x = if x = a then ↑(some b) else f x

@[simp]

theorem MeasureTheory.NoAtoms'.PFun.Dom_insert {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} {b : β} : (insert f a b).Dom = Set.insert a f.Dom

theorem MeasureTheory.NoAtoms'.PFun.lt_insert {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} {b : β} (ha : a ∉ f.Dom) : f ≤ insert f a b ∧ ¬insert f a b ≤ f

theorem MeasureTheory.NoAtoms'.PFun.Prop_insert {α : Type u_1} {β : Type u_2} {f : α →. β} {a : α} {b : β} {p : α → β → Prop} (hf : ∀ (x : α) (hx : x ∈ f.Dom), p x (f.fn x hx)) (hb : p a b) : have g := insert f a b; ∀ (x : α) (hx : x ∈ g.Dom), p x (g.fn x hx)

def MeasureTheory.NoAtoms'.PFun.Monotone {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] (f : α →. β) : Prop

The property of a partial function f to be monotone, i.e. f a ≤ f b whenever a ≤ b and both a and b are in the domain of f.

Equations

• MeasureTheory.NoAtoms'.PFun.Monotone f = ∀ ⦃a b : α⦄ (ha : a ∈ f.Dom) (hb : b ∈ f.Dom), a ≤ b → f.fn a ha ≤ f.fn b hb

theorem MeasureTheory.NoAtoms'.PFun.Monotone.Monotone {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α →. β} (hf : PFun.Monotone f) : _root_.Monotone fun (x : ↑f.Dom) => f.fn ↑x ⋯

theorem MeasureTheory.NoAtoms'.PFun.Monotone.insert {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α →. β} (hf : PFun.Monotone f) {a : α} {b : β} (hb : ∀ x ≤ a, ∀ (hx : x ∈ f.Dom), f.fn x hx ≤ b) (hb' : ∀ x ≥ a, ∀ (hx : x ∈ f.Dom), b ≤ f.fn x hx) : PFun.Monotone (PFun.insert f a b)

instance MeasureTheory.NoAtoms'.TopologicalSpace.SeparableSpace.subtype {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X} : TopologicalSpace.SeparableSpace ↑s

instance MeasureTheory.NoAtoms'.ClosedIicTopology.subtype {α : Type u_1} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {p : α → Prop} : ClosedIicTopology (Subtype p)

instance MeasureTheory.NoAtoms'.instIsCountablyGenerated_atTop {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace.SeparableSpace α] : Filter.atTop.IsCountablyGenerated

instance MeasureTheory.NoAtoms'.instIsCountablyGenerated_atBot {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace.SeparableSpace α] : Filter.atBot.IsCountablyGenerated

theorem MeasureTheory.NoAtoms'.iInter_of_monotone_of_frequently {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_2} [Preorder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∃ᶠ (i : ι) in Filter.atBot, MeasurableSet (s i)) : MeasurableSet (⋂ (i : ι), s i)

theorem MeasureTheory.NoAtoms'.iInter_of_monotone {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_2} [Preorder ι] [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∀ (i : ι), MeasurableSet (s i)) : MeasurableSet (⋂ (i : ι), s i)

theorem MeasureTheory.NoAtoms'.exists_measurable_sets_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] : ∃ (Ts : ↑(Set.Iic (μ Set.univ)) → Set α), Monotone Ts ∧ ∀ (x : ↑(Set.Iic (μ Set.univ))), MeasurableSet (Ts x) ∧ μ (Ts x) = ↑x

theorem MeasureTheory.NoAtoms'.exists_measurable_set_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {x : ENNReal} (ub : x ≤ μ Set.univ) : ∃ (s : Set α), MeasurableSet s ∧ μ s = x

theorem MeasureTheory.NoAtoms'.exists_measurable_subset_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {t : Set α} (ht : NullMeasurableSet t μ) {x : ENNReal} (ub : x ≤ μ t) : ∃ s ⊆ t, MeasurableSet s ∧ μ s = x

theorem MeasureTheory.NoAtoms'.exists_measurable_between_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s t : Set α} (hs : MeasurableSet s) (ht : NullMeasurableSet t μ) (h : s ⊆ t) {x : ENNReal} (lb : μ s ≤ x) (ub : x ≤ μ t) : ∃ (u : Set α), MeasurableSet u ∧ s ⊆ u ∧ u ⊆ t ∧ μ u = x

theorem MeasureTheory.NoAtoms'.exists_nullmeasurable_between_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (h : s ⊆ t) {x : ENNReal} (lb : μ s ≤ x) (ub : x ≤ μ t) : ∃ (u : Set α), NullMeasurableSet u μ ∧ s ⊆ u ∧ u ⊆ t ∧ μ u = x