ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B : BilinForm R M<GOAL>B.Nondegenerate ↔ ker B = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B : BilinForm R M<GOAL>B.Nondegenerate ↔ ∀ (m : M), B m = 0 → m = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>x : P<GOAL>inversion c R (inversion c R x) = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x✝ y z : P<VAR>r R✝ R : ℝ<VAR>hR : R ≠ 0<VAR>x : P<GOAL>inversion x R (inversion x R x) = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>x : P<VAR>hne : x ≠ c<GOAL>inversion c R (inversion c R x) = x
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<GOAL>(spectrum K f).Finite
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<GOAL>spectrum K = HasEigenvalue
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f✝ f : End K V<VAR>x : K<GOAL>x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : AddGroup G<VAR>f g : α →₀ G<GOAL>(f - g).support ⊆ f.support ∪ g.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : AddGroup G<VAR>f g : α →₀ G<GOAL>(f + -g).support ⊆ f.support ∪ (-g).support
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>↑((o.kahler x) y).arg + ↑((o.kahler y) z).arg = ↑((o.kahler x) z).arg
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>↑(↑‖y‖ ^ 2 * (o.kahler x) z).arg = ↑((o.kahler x) z).arg
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(o.kahler x) y ≠ 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(o.kahler y) z ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : y ∈ EMetric.ball x r<GOAL>CPolynomialAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : y ∈ EMetric.ball x r<VAR>this : ↑‖y - x‖₊ < r<GOAL>CPolynomialAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : y ∈ EMetric.ball x r<VAR>this✝ : ↑‖y - x‖₊ < r<VAR>this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - ↑‖y - x‖₊)<GOAL>CPolynomialAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>x y : E<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>h : y ∈ EMetric.ball x r<VAR>this✝ : ↑‖y - x‖₊ < r<VAR>this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - ↑‖y - x‖₊)<GOAL>CPolynomialAt 𝕜 f y
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p (n + 1) = count p n ↔ ¬p n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<GOAL>Measurable fun x => liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this : Countable (Subtype p)<GOAL>Measurable fun x => liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this : Countable (Subtype p)<VAR>hp : IsEmpty (Subtype p)<GOAL>Measurable fun x => liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<GOAL>Measurable fun x => liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<GOAL>Measurable fun x => liminf (fun x_1 => f x_1 x) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<GOAL>Measurable fun x => if ∀ (j : Subtype p), ¬BddBelow (range fun i => f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<GOAL>Measurable fun x => if ∀ (j : Subtype p), ¬BddBelow (range fun i => f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<GOAL>Measurable fun x => if ∀ (j : Subtype p), ¬BddBelow (range fun i => f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<GOAL>Measurable fun x => if ∀ (j : Subtype p), ¬BddBelow (range fun i => f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<GOAL>Measurable fun x => if ∀ (j : Subtype p), ¬BddBelow (range fun i => f (↑i) x) then sSup ∅ else ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<GOAL>Measurable fun x => ⨆ j, ⨅ i, f (↑i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<GOAL>Measurable fun b => ⨅ i, f (↑i) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<GOAL>Measurable fun b => ⨅ i, f (↑i) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<GOAL>Measurable fun b => ⨅ i, f (↑i) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<VAR>F1 : δ → α := fun x => F0 (reparam x j) x<VAR>hF1 : F1 = fun x => F0 (reparam x j) x<GOAL>Measurable F1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<VAR>F1 : δ → α := fun x => F0 (reparam x j) x<VAR>hF1 : F1 = fun x => F0 (reparam x j) x<VAR>g : ℕ → Subtype p := Classical.choose ⋯<GOAL>Measurable F1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝¹ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this✝ : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<VAR>F1 : δ → α := fun x => F0 (reparam x j) x<VAR>hF1 : F1 = fun x => F0 (reparam x j) x<VAR>g : ℕ → Subtype p := Classical.choose ⋯<VAR>Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k<VAR>this : F1 = fun x => if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x<GOAL>Measurable fun x => if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x