ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H ≫ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<VAR>l : Y ⟶ X<VAR>hl : l ≫ f = g<GOAL>l = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq f g e).inv = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g<VAR>e : Set.range ⇑f.base = Set.range ⇑g.base<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq f g e).hom = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift g f ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f).toPresheafedSpace = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f).base = f.base
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpaceHom Y f).c = f.c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y f = X
<VAR>X : AlgebraicGeometry.PresheafedSpace CommRingCat<VAR>Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f).toSheafedSpace = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace Y.toSheafedSpace f
<VAR>X : AlgebraicGeometry.PresheafedSpace CommRingCat<VAR>Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f).val = f
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.val = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>CategoryTheory.IsIso (f.c.app (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.ConcreteCategory C<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)<GOAL>AlgebraicGeometry.SheafedSpace.IsOpenImmersion f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ), (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).hom.c.app X_1 = f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop X_1))) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).inv ≫ f = Y.ofRestrict ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map i ≫ AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V) = AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U) ≫ Y.presheaf.map ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).op.map i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<GOAL>CategoryTheory.inv (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U) = f.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<GOAL>AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U ≫ f.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) = X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace<GOAL>f.c.app (Opposite.op U) ≫ AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>f.c.app (Opposite.op U) ≫ AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.SheafedSpace C<VAR>Y : TopCat<VAR>f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace<GOAL>AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f<VAR>h' : CategoryTheory.Epi f.base<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>ι : Type v<VAR>F : CategoryTheory.Discrete ι ⥤ AlgebraicGeometry.SheafedSpace C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : CategoryTheory.Discrete ι<GOAL>OpenEmbedding ⇑(CategoryTheory.Limits.colimit.ι F i).base
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>ι : Type v<VAR>F : CategoryTheory.Discrete ι ⥤ AlgebraicGeometry.SheafedSpace C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i j : CategoryTheory.Discrete ι<VAR>h : i ≠ j<VAR>U : TopologicalSpace.Opens ↑↑(F.obj i).toPresheafedSpace<GOAL>(TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι (F ⋙ AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace) j).base).obj ((TopologicalSpace.Opens.map (CategoryTheory.preservesColimitIso AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace F).inv.base).obj (⋯.functor.obj U)) = ⊥
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H' ≫ f = g
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>l : Y ⟶ X<VAR>hl : l ≫ f = g<GOAL>l = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H'
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>Set.range ⇑(AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H').val.base = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.val.base<VAR>stalk_iso : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)<GOAL>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).inv ≫ f = Y.ofRestrict ⋯
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>U V : (TopologicalSpace.Opens ↑X.toTopCat)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map i ≫ AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop V) = AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop U) ≫ Y.presheaf.map ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).op.map i)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑X.toTopCat<GOAL>CategoryTheory.inv (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U) = f.val.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U)) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f U ≫ f.val.c.app (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U)) = X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<GOAL>f.val.c.app (Opposite.op U) ≫ AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.val.base).obj U) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>hU : ↑U ⊆ Set.range ⇑f.val.base<GOAL>f.val.c.app (Opposite.op U) ≫ AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.val.base).obj U) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>Y : TopCat<VAR>f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace<GOAL>AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (Opposite.op U))
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f<VAR>h' : CategoryTheory.Epi f.val.base<GOAL>CategoryTheory.IsIso f
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>self : ProbabilityTheory.IsRatStieltjesPoint f a<VAR>t : ℚ<GOAL>⨅ r, f a ↑r = f a t
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>self : ProbabilityTheory.IsRatStieltjesPoint f a<GOAL>Filter.Tendsto (f a) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>self : ProbabilityTheory.IsRatStieltjesPoint f a<GOAL>Filter.Tendsto (f a) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>self : ProbabilityTheory.IsRatStieltjesPoint f a<GOAL>Monotone (f a)
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<GOAL>ProbabilityTheory.IsRatStieltjesPoint (fun p => f p.2) ((), a) ↔ ProbabilityTheory.IsRatStieltjesPoint f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<GOAL>MeasurableSet {a | ProbabilityTheory.IsRatStieltjesPoint f a}
<VAR>α : Type u_1<VAR>f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hf : p a → ProbabilityTheory.IsRatStieltjesPoint f a<VAR>hg : ¬p a → ProbabilityTheory.IsRatStieltjesPoint g a<GOAL>ProbabilityTheory.IsRatStieltjesPoint (fun a => if p a then f a else g a) a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>self : ProbabilityTheory.IsMeasurableRatCDF f<GOAL>Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>self : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>ProbabilityTheory.IsRatStieltjesPoint f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>q : ℚ<GOAL>0 ≤ f a q
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>q : ℚ<GOAL>f a q ≤ 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>Filter.Tendsto (f a) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>Filter.Tendsto (f a) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>q : ℚ<GOAL>⨅ r, f a ↑r = f a q
<VAR>q : ℚ<GOAL>0 ≤ ProbabilityTheory.defaultRatCDF q
<VAR>q : ℚ<GOAL>ProbabilityTheory.defaultRatCDF q ≤ 1
<GOAL>Filter.Tendsto ProbabilityTheory.defaultRatCDF Filter.atTop (𝓝 1)
<GOAL>Filter.Tendsto ProbabilityTheory.defaultRatCDF Filter.atBot (𝓝 0)
<VAR>t : ℚ<GOAL>⨅ r, ProbabilityTheory.defaultRatCDF ↑r = ProbabilityTheory.defaultRatCDF t
<VAR>α : Type u_1<VAR>a : α<GOAL>ProbabilityTheory.IsRatStieltjesPoint (fun x => ProbabilityTheory.defaultRatCDF) a
<VAR>α : Type u_4<VAR>MeasurableSpace α<GOAL>ProbabilityTheory.IsMeasurableRatCDF fun x q => ProbabilityTheory.defaultRatCDF q
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>h : ProbabilityTheory.IsRatStieltjesPoint f a<VAR>q : ℚ<GOAL>ProbabilityTheory.toRatCDF f a q = f a q
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<GOAL>Measurable (ProbabilityTheory.toRatCDF f)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<GOAL>ProbabilityTheory.IsMeasurableRatCDF (ProbabilityTheory.toRatCDF f)
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<GOAL>ProbabilityTheory.toRatCDF (fun p => f p.2) ((), a) = ProbabilityTheory.toRatCDF f a
<VAR>α : Type u_4<VAR>f : α → ℚ → ℝ<VAR>a : α<VAR>x : ℝ<GOAL>ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a x = ⨅ q, f a ↑q
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<GOAL>ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a = fun t => ⨅ r, f a ↑r
<VAR>α : Type u_1<VAR>f : α → ℚ → ℝ<VAR>a : α<GOAL>ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux (fun p => f p.2) ((), a) = ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a ↑r = f a r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℝ<GOAL>0 ≤ ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>Monotone (ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>ContinuousWithinAt (ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a) (Set.Ici x) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℚ<GOAL>↑(hf.stieltjesFunction a) ↑r = f a r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℝ<GOAL>0 ≤ ↑(hf.stieltjesFunction a) r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>↑(hf.stieltjesFunction a) x ≤ 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>x : ℝ<GOAL>Measurable fun a => ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>x : ℝ<GOAL>MeasureTheory.StronglyMeasurable fun a => ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>(hf.stieltjesFunction a).measure (Set.Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<VAR>a : α<GOAL>(hf.stieltjesFunction a).measure Set.univ = 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : ProbabilityTheory.IsMeasurableRatCDF f<GOAL>Measurable fun a => (hf.stieltjesFunction a).measure
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<VAR>r : ℚ<GOAL>↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) ↑r = ProbabilityTheory.toRatCDF f a r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>ProbabilityTheory.stieltjesOfMeasurableRat (fun p => f p.2) ⋯ ((), a) = ProbabilityTheory.stieltjesOfMeasurableRat f hf a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<VAR>r : ℝ<GOAL>0 ≤ ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) r
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x ≤ 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>Filter.Tendsto (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a)) Filter.atBot (𝓝 0)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>Filter.Tendsto (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>x : ℝ<GOAL>Measurable fun a => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>x : ℝ<GOAL>MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<VAR>x : ℝ<GOAL>(ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure (Set.Iic x) = ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>(ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure Set.univ = 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun a => (ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂ρ.fst, (κ x) s = (ρ.condKernel x) s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>ρ : MeasureTheory.Measure (α × ℝ)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>κ : ProbabilityTheory.Kernel α ℝ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>ρ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel ρ<VAR>κ : ProbabilityTheory.Kernel (α × β) Ω<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<GOAL>(fun b => κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<GOAL>(fun b => κ.condKernel (a, b)) =ᵐ[κ.fst a] ⇑(κ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>MeasurableSpace.CountableOrCountablyGenerated α β<VAR>ρ : MeasureTheory.Measure (β × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>a : α<GOAL>(fun b => (ProbabilityTheory.Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel