ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<VAR>b : β<VAR>h : ∀ (a' : α), r a' a → s (↑(f.collapseF a')) b<GOAL>¬s b ↑(let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑((fun y x => ⋯.fix (fun a IH => let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) y) a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<VAR>b : β<VAR>h : ∀ (a' : α), r a' a → s (↑(f.collapseF a')) b<GOAL>¬s b (⋯.min {b | ∀ (a_1 : α), r a_1 a → s (↑(⋯.fix (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1)) b} ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
<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>hf : AnalyticAt 𝕜 f x<VAR>hg : AnalyticAt 𝕜 g x<GOAL>AnalyticAt 𝕜 (f - g) x
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f✝ : Filter τ<VAR>ϕ✝ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>inst✝ : TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s<VAR>hgc : Continuous gb<GOAL>MapsTo gb (ω f ϕ s) (ω f ϕ' s')
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f✝ : Filter τ<VAR>ϕ✝ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>inst✝ : TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s<VAR>hgc : Continuous gb<GOAL>∀ ⦃x : β⦄, (∀ i ∈ f, x ∈ closure (image2 ϕ i s)) → ∀ i ∈ f, gb x ∈ closure (image2 ϕ' i s')
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f✝ : Filter τ<VAR>ϕ✝ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>inst✝ : TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s<VAR>hgc : Continuous gb<VAR>y : β<VAR>hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)<VAR>u : Set τ<VAR>hu : u ∈ f<GOAL>gb y ∈ closure (image2 ϕ' u s')
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f✝ : Filter τ<VAR>ϕ✝ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>inst✝ : TopologicalSpace β'<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>ϕ' : τ → α' → β'<VAR>ga : α → α'<VAR>s' : Set α'<VAR>hs : MapsTo ga s s'<VAR>gb : β → β'<VAR>hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s<VAR>hgc : Continuous gb<VAR>y : β<VAR>hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>t : τ<VAR>ht : t ∈ u ∩ {x | (fun t => EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}<VAR>x : α<VAR>hx : x ∈ s<GOAL>gb (ϕ t x) ∈ image2 ϕ' u s'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>f : (Step k n)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>∃ x, Polynomial.eval₂ (toStepSucc k n) x f = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>f : (Step k n)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<VAR>x : AdjoinMonic (Step k n)<VAR>hx : Polynomial.eval₂ (toAdjoinMonic (Step k n)) x f = 0<GOAL>∃ x, Polynomial.eval₂ (toStepSucc k n) x f = 0
<VAR>p : Nat<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>x✝.atEnd { byteIdx := p } = true ↔ p = x✝.toString.utf8ByteSize
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : a ∉ m.snd<GOAL>↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : a ∉ m.snd<GOAL>filter (fun x => a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : a ∉ m.snd<GOAL>∀ (a_1 : α), a_1 ∉ filter (fun x => a ≠ x) ↑(replicate (↑m.fst) a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m✝ : ℕ<VAR>s : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>m : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : a ∉ m.snd<GOAL>∀ a_1 ∈ ↑m.snd, a ≠ a_1
<VAR>α : Type u<VAR>β✝ : Type v<VAR>δ : Type w<VAR>a : α<VAR>β : Type u<VAR>fr : Stream' α → β<VAR>ch : fr (iterate id a) = fr (const a)<GOAL>fr (iterate id a).tail = fr (const a).tail
<VAR>α : Type u<VAR>β✝ : Type v<VAR>δ : Type w<VAR>a : α<VAR>β : Type u<VAR>fr : Stream' α → β<VAR>ch : fr (iterate id a) = fr (const a)<GOAL>fr (iterate id (id a)) = fr (const a)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : finrank K ↥s + finrank K ↥t = finrank K V<VAR>hdisjoint : Disjoint s t<GOAL>s ⊔ t = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : finrank K ↥s + finrank K ↥t = finrank K V<VAR>hdisjoint : Disjoint s t<VAR>h_finrank_inf : finrank K ↥(s ⊓ t) = 0<GOAL>s ⊔ t = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : finrank K ↥s + finrank K ↥t = finrank K V<VAR>hdisjoint : Disjoint s t<VAR>h_finrank_inf : finrank K ↥(s ⊓ t) = 0<GOAL>finrank K ↥(s ⊔ t) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : finrank K ↥s + finrank K ↥t = finrank K V<VAR>hdisjoint : Disjoint s t<VAR>h_finrank_inf : finrank K ↥(s ⊓ t) = 0<GOAL>finrank K ↥(s ⊔ t) = finrank K ↥s + finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : finrank K ↥s + finrank K ↥t = finrank K V<VAR>hdisjoint : Disjoint s t<VAR>h_finrank_inf : finrank K ↥(s ⊓ t) = 0<GOAL>finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₂ k₁ k₀ : ι<VAR>r₂₁ : c.Rel k₂ k₁<VAR>r₁₀ : c.Rel k₁ k₀<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₂ k₁ k₀ : ι<VAR>r₂₁ : c.Rel k₂ k₁<VAR>r₁₀ : c.Rel k₁ k₀<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) + (dite (c.Rel k₂ k₁) (h k₁ k₂) fun x => 0) ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>¬2 * n % 2 = (2 * m + 1) % 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<VAR>x : Fin (n + 1)<GOAL>∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<VAR>x : Fin (n + 1)<GOAL>f x * ∏ x_1 : Fin n, f (x.succAboveEmb x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>xs : List (Sigma β)<VAR>tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs<VAR>fst_i : α<VAR>snd_i : β fst_i<GOAL>a ∈ (⟨fst_i, snd_i⟩ :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ ⟨fst_i, snd_i⟩ :: xs
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>xs : List (Sigma β)<VAR>tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs<VAR>fst_i : α<VAR>snd_i : β fst_i<GOAL>(a = fst_i ∨ ∃ b, ⟨a, b⟩ ∈ xs) ↔ (a = fst_i ∧ ∃ x, HEq x snd_i) ∨ ∃ x, ⟨a, x⟩ ∈ xs
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>xs : List (Sigma β)<VAR>tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs<VAR>fst_i : α<VAR>snd_i : β fst_i<GOAL>a = fst_i → ∃ x, HEq x snd_i
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>xs : List (Sigma β)<VAR>tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs<VAR>snd_i : β a<GOAL>∃ x, HEq x snd_i
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>H : ∀ (i : ι), f i < sup f<GOAL>(sup f).cof ≤ #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>H : ∀ (i : ι), f i < sup f<GOAL>(sup f).cof ≤ Cardinal.lift.{u, u} #ι
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>h : DifferentiableAt ℝ abs 0<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>h : DifferentiableAt ℝ abs 0<VAR>h₁ : deriv abs 0 = 1<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>h : DifferentiableAt ℝ abs 0<VAR>h₁ : deriv abs 0 = 1<VAR>h₂ : deriv abs 0 = -1<GOAL>False
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>(f - g).neLocus f = g.support
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>s : Set S<VAR>N : Submodule R M<GOAL>s • N = ⨆ a ∈ s, a • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>s : Set S<VAR>N : Submodule R M<GOAL>{p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>S : Type u_4<VAR>inst✝⁴ : Monoid S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DistribMulAction S M<VAR>sR : Set R<VAR>s✝ : Set S<VAR>N✝ : Submodule R M<VAR>inst✝ : SMulCommClass S R M<VAR>s : Set S<VAR>N : Submodule R M<GOAL>{p | ∀ ⦃r : S⦄, r ∈ s → ∀ a ∈ N, r • a ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), T1Space (β i)<GOAL>ClosedEmbedding (update x i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), T1Space (β i)<GOAL>Continuous (update x i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), T1Space (β i)<GOAL>Injective (update x i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → TopologicalSpace (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>inst✝ : ∀ (i : ι), T1Space (β i)<GOAL>IsClosedMap (update x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s₁ s₂ s₃ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ s₃ ∩ s₂
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>s : Multiset α<VAR>h : LeftCommutative f<VAR>b : β<GOAL>noncommFoldr f s ⋯ b = foldr f h b s
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>h : LeftCommutative f<VAR>b : β<VAR>a✝ : List α<GOAL>noncommFoldr f ⟦a✝⟧ ⋯ b = foldr f h b ⟦a✝⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>(∀ᵐ (x : α) ∂μ, x ∈ s → x ∈ t) ↔ μ (s \ t) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ {a | a ∈ s ∧ a ∉ t} = 0 ↔ μ (s \ t) = 0
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<VAR>this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ S, ↑m ≤ y * ↑d}<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<VAR>this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ S, ↑m ≤ y * ↑d}<VAR>f : ℕ → ℤ<VAR>hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d}, z ≤ f d<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<VAR>this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ S, ↑m ≤ y * ↑d}<VAR>f : ℕ → ℤ<VAR>hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d}, z ≤ f d<VAR>hf₁ : ∀ n > 0, ∃ y ∈ S, ↑(↑(f n) / ↑n) ≤ y<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<VAR>this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ S, ↑m ≤ y * ↑d}<VAR>f : ℕ → ℤ<VAR>hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d}, z ≤ f d<VAR>hf₁ : ∀ n > 0, ∃ y ∈ S, ↑(↑(f n) / ↑n) ≤ y<VAR>hf₂ : ∀ n > 0, ∀ y ∈ S, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)<GOAL>∃ x, IsLUB S x
<VAR>S : Set ℝ<VAR>L : ℝ<VAR>hL : L ∈ S<VAR>U : ℝ<VAR>hU : U ∈ upperBounds S<VAR>this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ S, ↑m ≤ y * ↑d}<VAR>f : ℕ → ℤ<VAR>hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ S, ↑m ≤ y * ↑d}, z ≤ f d<VAR>hf₁ : ∀ n > 0, ∃ y ∈ S, ↑(↑(f n) / ↑n) ≤ y<VAR>hf₂ : ∀ n > 0, ∀ y ∈ S, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)<VAR>hg : IsCauSeq abs fun n => ↑(f n) / ↑n<GOAL>∃ x, IsLUB S x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = μ ↔ μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<GOAL>μ.singularPart ν = μ ↔ μ ⟂ₘ ν
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (map (fun f => f x) l).prod) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<GOAL>𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>A : Type u_3<VAR>inst✝ : TopologicalSpace A<VAR>f₀ f₁ : C(A, α)<VAR>g₀ g₁ : C(A, β)<VAR>S : Set A<VAR>F : f₀.Homotopy f₁<VAR>G : g₀.Homotopy g₁<VAR>x : A<GOAL>{ toFun := fun t => (F t, G t), continuous_toFun := ⋯ }.toFun (0, x) = (f₀.prodMk g₀) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>A : Type u_3<VAR>inst✝ : TopologicalSpace A<VAR>f₀ f₁ : C(A, α)<VAR>g₀ g₁ : C(A, β)<VAR>S : Set A<VAR>F : f₀.Homotopy f₁<VAR>G : g₀.Homotopy g₁<VAR>x : A<GOAL>{ toFun := fun t => (F t, G t), continuous_toFun := ⋯ }.toFun (1, x) = (f₁.prodMk g₁) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<GOAL>fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>r s : R<VAR>j : J<GOAL>colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ (↑{ toFun := fun r => colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun (r + s) = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ ((↑{ toFun := fun r => colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun r + (↑{ toFun := fun r => colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun s)
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>r s : R<VAR>j : J<GOAL>((F.obj j).smul r + (F.obj j).smul s) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ (colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ } + colimMap { app := fun j => (F.obj j).smul s, naturality := ⋯ })
<VAR>R : Type w<VAR>inst✝² : Ring R<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrp)<VAR>r s : R<VAR>j : J<GOAL>(F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j + (F.obj j).smul s ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ } + colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrp) j ≫ colimMap { app := fun j => (F.obj j).smul s, naturality := ⋯ }
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<GOAL>Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<VAR>hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C<GOAL>Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<VAR>hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C<VAR>hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ<GOAL>Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<VAR>hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C<VAR>hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ<VAR>hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)<GOAL>Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<VAR>hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C<VAR>hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ<VAR>hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)<VAR>i : ℕ<GOAL>0 ≤ᶠ[ae μ] μ[∑ k ∈ Finset.range (i + 1), ξ k * (f (k + 1) - f k) - ∑ k ∈ Finset.range i, ξ k * (f (k + 1) - f k)|↑𝒢 i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>R : ℝ<VAR>ξ f : ℕ → Ω → ℝ<VAR>hf : Submartingale f 𝒢 μ<VAR>hξ : Adapted 𝒢 ξ<VAR>hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R<VAR>hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω<VAR>hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C<VAR>hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ<VAR>hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)<VAR>i : ℕ<GOAL>0 ≤ᶠ[ae μ] μ[ξ i * (f (i + 1) - f i)|↑𝒢 i]