ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → α<GOAL>MeasurableSpace.comap g ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ m₂ : MeasurableSpace α<VAR>g : β → α<GOAL>MeasurableSpace.comap g (m₁ ⊔ m₂) = MeasurableSpace.comap g m₁ ⊔ MeasurableSpace.comap g m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort uι<VAR>g : β → α<VAR>m : ι → MeasurableSpace α<GOAL>MeasurableSpace.comap g (⨆ i, m i) = ⨆ i, MeasurableSpace.comap g (m i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>MeasurableSpace.map f ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ m₂ : MeasurableSpace α<VAR>f : α → β<GOAL>MeasurableSpace.map f (m₁ ⊓ m₂) = MeasurableSpace.map f m₁ ⊓ MeasurableSpace.map f m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort uι<VAR>f : α → β<VAR>m : ι → MeasurableSpace α<GOAL>MeasurableSpace.map f (⨅ i, m i) = ⨅ i, MeasurableSpace.map f (m i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → β<GOAL>MeasurableSpace.comap f (MeasurableSpace.map f m) ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>g : β → α<GOAL>m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>b : β<GOAL>MeasurableSpace.map (fun _a => b) m = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace β<VAR>b : β<GOAL>MeasurableSpace.comap (fun _a => b) m = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set (Set β)<GOAL>MeasurableSpace.comap f (MeasurableSpace.generateFrom s) = MeasurableSpace.generateFrom (Set.preimage f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ : MeasurableSpace α<VAR>m₂ : MeasurableSpace β<VAR>f : α → β<GOAL>Measurable f ↔ m₂ ≤ MeasurableSpace.map f m₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ : MeasurableSpace α<VAR>m₂ : MeasurableSpace β<VAR>f : α → β<GOAL>Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace β<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ma ma' : MeasurableSpace α<VAR>mb mb' : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>ha : ma ≤ ma'<VAR>hb : mb' ≤ mb<GOAL>Measurable f
<VAR>α : Type u_1<VAR>m mα : MeasurableSpace α<VAR>hm : m ≤ mα<GOAL>Measurable id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>s : Set (Set β)<VAR>f : α → β<VAR>h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Subsingleton α<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Subsingleton β<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Zero α<GOAL>Measurable 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>One α<GOAL>Measurable 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>IsEmpty α<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>IsEmpty β<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : ∀ (x y : β), f x = f y<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>NatCast α<VAR>n : ℕ<GOAL>Measurable ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>IntCast α<VAR>n : ℤ<GOAL>Measurable ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Countable α<VAR>MeasurableSingletonClass α<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>Finite α<VAR>MeasurableSingletonClass α<VAR>f : α → β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>hf : Measurable f<VAR>n : ℕ<GOAL>Measurable f^[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>t : Set β<VAR>hf : Measurable f<VAR>ht : MeasurableSet t<GOAL>MeasurableSet (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>hf : Measurable f<GOAL>MeasurableSet (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>∀ {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (s.piecewise f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>p : α → Prop<GOAL>∀ {x : DecidablePred p}, MeasurableSet {a | p a} → Measurable f → Measurable g → Measurable fun x_1 => if p x_1 then f x_1 else g x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Zero β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<GOAL>Measurable (s.indicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Zero β<VAR>MeasurableSingletonClass β<VAR>b : β<VAR>NeZero b<GOAL>Measurable (s.indicator fun x => b) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>One β<VAR>MeasurableSingletonClass β<VAR>hf : Measurable f<GOAL>MeasurableSet (Function.mulSupport f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Zero β<VAR>MeasurableSingletonClass β<VAR>hf : Measurable f<GOAL>MeasurableSet (Function.support f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Countable α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Countable α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : Unit → α<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Measurable ULift.down
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>Measurable ULift.up
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set (ULift.{u_6, u_1} α)<GOAL>MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : ℕ → α<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℕ<GOAL>(∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → Bool<VAR>h : MeasurableSet (f ⁻¹' {true})<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → Prop<VAR>h : MeasurableSet (f ⁻¹' {True})<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>(x : α) → DecidablePred (p x)<VAR>N : ℕ<VAR>hN : ∀ k ≤ N, MeasurableSet {x | Nat.findGreatest (p x) N = k}<GOAL>Measurable fun x => Nat.findGreatest (p x) N
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>(x : α) → DecidablePred (p x)<VAR>N : ℕ<VAR>hN : ∀ k ≤ N, MeasurableSet {x | p x k}<GOAL>Measurable fun x => Nat.findGreatest (p x) N
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>(x : α) → DecidablePred (p x)<VAR>hp : ∀ (x : α), ∃ N, p x N<VAR>hm : ∀ (k : ℕ), MeasurableSet {x | p x k}<GOAL>Measurable fun x => Nat.find ⋯
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Setoid α<VAR>t : Set (Quotient s)<GOAL>MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>s : Setoid α<VAR>f : Quotient s → β<GOAL>Measurable f ↔ Measurable (f ∘ Quotient.mk'')
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Setoid α<GOAL>Measurable Quotient.mk'
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Setoid α<GOAL>Measurable Quotient.mk''
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>r : α → α → Prop<GOAL>Measurable (Quot.mk r)
<VAR>G : Type u_6<VAR>Group G<VAR>MeasurableSpace G<VAR>S : Subgroup G<GOAL>Measurable QuotientGroup.mk
<VAR>G : Type u_6<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>S : AddSubgroup G<GOAL>Measurable QuotientAddGroup.mk
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>G : Type u_6<VAR>Group G<VAR>MeasurableSpace G<VAR>S : Subgroup G<VAR>f : G ⧸ S → α<GOAL>Measurable f ↔ Measurable (f ∘ QuotientGroup.mk)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>G : Type u_6<VAR>AddGroup G<VAR>MeasurableSpace G<VAR>S : AddSubgroup G<VAR>f : G ⧸ S → α<GOAL>Measurable f ↔ Measurable (f ∘ QuotientAddGroup.mk)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → Prop<GOAL>Measurable Subtype.val
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>t : Set ↑s<VAR>h : MeasurableSet (Subtype.val '' t)<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : Set α<VAR>t : Set ↑s<VAR>hs : MeasurableSet s<GOAL>MeasurableSet t → MeasurableSet (Subtype.val '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>p : β → Prop<VAR>f : α → Subtype p<VAR>hf : Measurable f<GOAL>Measurable fun a => ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Measurable f<VAR>h : ∀ (x : α), p (f x)<GOAL>Measurable fun x => ⟨f x, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<GOAL>Measurable (Set.rangeFactorization f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>hf : Measurable f<VAR>hpq : ∀ (x : α), p x → q (f x)<GOAL>Measurable (Subtype.map f hpq)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>Measurable (Set.inclusion h)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>u : Set ↑s<VAR>hs : MeasurableSet (Subtype.val ⁻¹' s)<VAR>hu : MeasurableSet u<GOAL>MeasurableSet (Set.inclusion h '' u)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>u : Set ↑s<VAR>hs : MeasurableSet s<VAR>hu : MeasurableSet u<GOAL>MeasurableSet (Set.inclusion h '' u)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t u : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : Set.univ ⊆ s ∪ t<VAR>hsu : MeasurableSet (Subtype.val ⁻¹' u)<VAR>htu : MeasurableSet (Subtype.val ⁻¹' u)<GOAL>MeasurableSet u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : Set.univ ⊆ s ∪ t<VAR>hc : Measurable fun a => f ↑a<VAR>hd : Measurable fun a => f ↑a<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h₁ : Measurable (s.restrict f)<VAR>h₂ : Measurable (sᶜ.restrict f)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>(x : α) → Decidable (x ∈ s)<VAR>f : ↑s → β<VAR>hf : Measurable f<VAR>g : ↑sᶜ → β<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Finite<VAR>hf : Measurable (sᶜ.restrict f)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>f : α → β<VAR>a : α<VAR>hf : Measurable ({x | x ≠ a}.restrict f)<GOAL>Measurable f
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>x : β<GOAL>x ∈ measurableAtom x
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>x y : β<VAR>h : y ∈ measurableAtom x<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hxs : x ∈ s<GOAL>y ∈ s
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>s : Set β<VAR>x : β<VAR>hs : MeasurableSet s<VAR>hx : x ∈ s<GOAL>measurableAtom x ⊆ s
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>MeasurableSingletonClass β<VAR>x : β<GOAL>measurableAtom x = {x}
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>Countable β<VAR>x : β<GOAL>MeasurableSet (measurableAtom x)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf : Measurable f<GOAL>Measurable fun a => (f a).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf : Measurable f<GOAL>Measurable fun a => (f a).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<VAR>hf₁ : Measurable fun a => (f a).1<VAR>hf₂ : Measurable fun a => (f a).2<GOAL>Measurable f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>β : Type u_6<VAR>γ : Type u_7<GOAL>∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : α → β} {g : α → γ}, Measurable f → Measurable g → Measurable fun a => (f a, g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (Prod.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>x : α<GOAL>Measurable (Prod.mk x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>y : β<GOAL>Measurable fun x => (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β → γ<VAR>hf : Measurable (Function.uncurry f)<VAR>x : α<GOAL>Measurable (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β → γ<VAR>hf : Measurable (Function.uncurry f)<VAR>y : β<GOAL>Measurable fun x => f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>f : α → β × γ<GOAL>Measurable f ↔ (Measurable fun a => (f a).1) ∧ Measurable fun a => (f a).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>Measurable Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>∀ {x : MeasurableSpace γ} {f : α × β → γ}, Measurable (f ∘ Prod.swap) ↔ Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>MeasurableSet (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set α<VAR>t : Set β<VAR>h : (s ×ˢ t).Nonempty<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set α<VAR>t : Set β<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set (α × β)<GOAL>MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable β<GOAL>∀ {x : MeasurableSpace γ} {f : α × β → γ}, (∀ (y : β), Measurable fun x => f (x, y)) → (∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)) → Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable β<VAR>MeasurableSingletonClass β<GOAL>∀ {x : MeasurableSpace γ} {f : α × β → γ}, (∀ (y : β), Measurable fun x => f (x, y)) → Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<GOAL>∀ {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
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort uι<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>t : ι → Set α<VAR>f : (i : ι) → ↑(t i) → β<VAR>htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ ⋃ i, t i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>hfm : ∀ (i : ι), Measurable (f i)<GOAL>Measurable (Set.iUnionLift t f htf T hT)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort uι<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>t : ι → Set α<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>f : (i : ι) → ↑(t i) → β<VAR>hfm : ∀ (i : ι), Measurable (f i)<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>htU : ⋃ i, t i = Set.univ<GOAL>Measurable (Set.liftCover t f hf htU)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>ι : Type u_6<VAR>Countable ι<VAR>Nonempty ι<VAR>t : ι → Set α<VAR>t_meas : ∀ (n : ι), MeasurableSet (t n)<VAR>g : ι → α → β<VAR>hg : ∀ (n : ι), Measurable (g n)<VAR>ht : Pairwise fun i j => Set.EqOn (g i) (g j) (t i ∩ t j)<GOAL>∃ f, Measurable f ∧ ∀ (n : ι), Set.EqOn f (g n) (t n)
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>MeasurableSpace α<VAR>(a : δ) → MeasurableSpace (π a)<VAR>g : α → (a : δ) → π a<GOAL>Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>a : δ<GOAL>Measurable fun f => f a
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>MeasurableSpace α<VAR>(a : δ) → MeasurableSpace (π a)<VAR>a : δ<VAR>g : α → (a : δ) → π a<VAR>hg : Measurable g<GOAL>Measurable fun x => g x a
<VAR>α : Type u_1<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>MeasurableSpace α<VAR>(a : δ) → MeasurableSpace (π a)<VAR>f : α → (a : δ) → π a<VAR>hf : ∀ (a : δ), Measurable fun c => f c a<GOAL>Measurable f
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>a : δ<VAR>DecidableEq δ<GOAL>Measurable fun p => Function.update p.1 a p.2
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>Unique δ<VAR>(i : δ) → MeasurableSpace (π i)<GOAL>Measurable uniqueElim
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>DecidableEq δ<VAR>s : Finset δ<VAR>x : (i : δ) → π i<GOAL>Measurable (Function.updateFinset x s)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>f : (a : δ) → π a<VAR>a : δ<VAR>DecidableEq δ<GOAL>Measurable (Function.update f a)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>a : δ<VAR>DecidableEq δ<VAR>x : π a<GOAL>Measurable fun x_1 => Function.update x_1 a x
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>i i' : δ<VAR>h : i = i'<GOAL>Measurable ⋯.mp
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>β : Type u_7<VAR>MeasurableSpace β<VAR>i i' : δ<VAR>h : i = i'<VAR>f : β → π i<VAR>hf : Measurable f<GOAL>Measurable fun x => ⋯.mp (f x)
<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>f : δ' ≃ δ<GOAL>Measurable ⇑(Equiv.piCongrLeft π f)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>ht : ∀ i ∈ s, MeasurableSet (t i)<GOAL>MeasurableSet (s.pi t)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>Countable δ<VAR>t : (i : δ) → Set (π i)<VAR>ht : ∀ (i : δ), MeasurableSet (t i)<GOAL>MeasurableSet (Set.univ.pi t)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>h : (s.pi t).Nonempty<GOAL>MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<GOAL>MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>p : δ → Prop<VAR>DecidablePred p<GOAL>Measurable ⇑(Equiv.piEquivPiSubtypeProd p π).symm
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(a : δ) → MeasurableSpace (π a)<VAR>p : δ → Prop<VAR>DecidablePred p<GOAL>Measurable ⇑(Equiv.piEquivPiSubtypeProd p π)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(x : δ) → MeasurableSpace (π x)<VAR>l : List δ<GOAL>Measurable (List.TProd.mk l)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(x : δ) → MeasurableSpace (π x)<VAR>DecidableEq δ<VAR>l : List δ<VAR>i : δ<VAR>hi : i ∈ l<GOAL>Measurable fun v => v.elim hi
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(x : δ) → MeasurableSpace (π x)<VAR>DecidableEq δ<VAR>l : List δ<VAR>h : ∀ (i : δ), i ∈ l<GOAL>Measurable (List.TProd.elim' h)
<VAR>δ : Type u_4<VAR>π : δ → Type u_6<VAR>(x : δ) → MeasurableSpace (π x)<VAR>l : List δ<VAR>s : (i : δ) → Set (π i)<VAR>hs : ∀ (i : δ), MeasurableSet (s i)<GOAL>MeasurableSet (Set.tprod l s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>Measurable Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<GOAL>Measurable Sum.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set (α ⊕ β)<GOAL>MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>∀ {x : MeasurableSpace γ} {f : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>∀ {x : MeasurableSpace γ} {f : α → γ} {g : β → γ}, Measurable f → Measurable g → Measurable (Sum.elim f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<GOAL>∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace δ} {f : α → β} {g : γ → δ}, Measurable f → Measurable g → Measurable (Sum.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set α<GOAL>MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set β<GOAL>MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace α<GOAL>MeasurableSet (Set.range Sum.inl)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace α<GOAL>MeasurableSet (Set.range Sum.inr)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → Prop<GOAL>MeasurableSet {a | p a} ↔ Measurable p
<VAR>α : Type u_1<VAR>s : Set α<VAR>MeasurableSpace α<GOAL>(Measurable fun x => x ∈ s) ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : α → Prop<VAR>hp : Measurable p<GOAL>Measurable fun x => ¬p x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>Measurable fun a => p a ∧ q a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>Measurable fun a => p a ∨ q a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>Measurable fun a => p a → q a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>Measurable fun a => p a ↔ q a