ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>α β : F ⟶ G<GOAL>F.a ≫ U.map (α.f + β.f) = (α.f + β.f) ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<GOAL>F.a ≫ U.map 0 = 0 ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>n : ℕ<VAR>α : F ⟶ G<GOAL>F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>α : F ⟶ G<GOAL>F.a ≫ U.map (-α.f) = (-α.f) ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>α β : F ⟶ G<GOAL>F.a ≫ U.map (α.f - β.f) = (α.f - β.f) ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>r : ℤ<VAR>α : F ⟶ G<GOAL>F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ b✝ c✝ : F ⟶ G<GOAL>(a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ : F ⟶ G<GOAL>(0 + a✝).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ : F ⟶ G<GOAL>(a✝ + 0).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>x✝ : F ⟶ G<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) 0 x✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>n✝ : ℕ<VAR>x✝ : F ⟶ G<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) (n✝ + 1) x✝).f = ((fun n α => { f := n • α.f, h := ⋯ }) n✝ x✝ + x✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ b✝ : F ⟶ G<GOAL>(a✝ - b✝).f = (a✝ + -b✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ : F ⟶ G<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) 0 a✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>↑(n✝ + 1) • a✝.f = ({ f := ↑n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>n✝ • a✝.f + a✝.f = ({ f := n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>n✝ : ℕ<VAR>a✝ : F ⟶ G<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) (Int.negSucc n✝) a✝).f = (-(fun r α => { f := r • α.f, h := ⋯ }) (↑n✝.succ) a✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ : F ⟶ G<GOAL>(-a✝ + a✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>F G : U.Coalgebra<VAR>a✝ b✝ : F ⟶ G<GOAL>(a✝ + b✝).f = (b✝ + a✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>P✝ Q✝ R✝ : U.Coalgebra<VAR>f✝ f'✝ : P✝ ⟶ Q✝<VAR>g✝ : Q✝ ⟶ R✝<GOAL>((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>T : Monad C<VAR>inst✝¹ : T.Additive<VAR>U : Comonad C<VAR>inst✝ : U.Additive<VAR>P✝ Q✝ R✝ : U.Coalgebra<VAR>f✝ : P✝ ⟶ Q✝<VAR>g✝ g'✝ : Q✝ ⟶ R✝<GOAL>(f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set Cᵒᵖ<GOAL>IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : (p.append q).IsTrail<GOAL>p.IsTrail
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : p.edges.Nodup ∧ q.edges.Nodup ∧ p.edges.Disjoint q.edges<GOAL>p.IsTrail
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_countable_range : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<GOAL>stoppedValue f τ =ᶠ[ae μ] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_countable_range : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}<GOAL>stoppedValue f τ =ᶠ[ae μ] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_countable_range : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}<GOAL>stoppedValue f τ =ᶠ[ae (μ.restrict Set.univ)] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_countable_range : (Set.range τ).Countable<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}<GOAL>∀ i ∈ Set.range τ, stoppedValue f τ =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f n|hτ.measurableSpace]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s t : Set α<GOAL>Sum.inr ⁻¹' range Sum.inl = ∅
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j✝ : J<GOAL>(biproduct.lift fun j => biproduct.π f j ▷ X) ≫ biproduct.π (fun j => f j ⊗ X) j✝ = (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j✝ : J<GOAL>biproduct.π f j✝ ▷ X = (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<GOAL>↑(map K.subtype (H.subgroupOf K)) = ↑(H ⊓ K)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<GOAL>↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<VAR>hg' : ∀ (x : G), 0 ≤ g' x<VAR>H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<GOAL>(f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<VAR>hg' : ∀ (x : G), 0 ≤ g' x<VAR>H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0<GOAL>(f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<VAR>hg' : ∀ (x : G), 0 ≤ g' x<VAR>H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0<GOAL>0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>X : ι → Type u_3<VAR>t : (i : ι) → TopologicalSpace (X i)<VAR>T : (i : ι) → Set (Set (X i))<VAR>cond : ∀ (i : ι), IsTopologicalBasis (T i)<VAR>f : (i : ι) → β → X i<GOAL>IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}
<VAR>β : Type u_1<VAR>ι : Type u_2<VAR>X : ι → Type u_3<VAR>t : (i : ι) → TopologicalSpace (X i)<VAR>T : (i : ι) → Set (Set (X i))<VAR>cond : ∀ (i : ι), IsTopologicalBasis (T i)<VAR>f : (i : ι) → β → X i<VAR>S : Set β<GOAL>(∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Nat.card G' ∣ Nat.card G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Nat.card (G ⧸ f.ker) ∣ Nat.card G
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>a b : ℝ<VAR>s : Set ℝ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f [[a, b]]<VAR>Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x<VAR>Hi : IntervalIntegrable f' volume a b<GOAL>∫ (x : ℝ) in a..b, f' x = f b - f a
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>a b : ℝ<VAR>s : Set ℝ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f [[a, b]]<VAR>Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x<VAR>Hi : IntervalIntegrable f' volume a b<VAR>hab : a ≤ b<GOAL>∫ (x : ℝ) in a..b, f' x = f b - f a
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>a b : ℝ<VAR>s : Set ℝ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f [[a, b]]<VAR>Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x<VAR>Hi : IntervalIntegrable f' volume a b<VAR>hab : b ≤ a<GOAL>∫ (x : ℝ) in a..b, f' x = f b - f a
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2
<VAR>α : Type u<VAR>inst✝³ : GroupWithZero α<VAR>a b : α<VAR>inst✝² : Invertible a<VAR>inst✝¹ : Invertible b<VAR>inst✝ : Invertible (a / b)<GOAL>a / b * (b / a) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>NullMeasurableSet {a | f a < g a} μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>{a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a | f a < g a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>x : α<VAR>hfx : f x = AEStronglyMeasurable.mk f hf x<VAR>hgx : g x = AEStronglyMeasurable.mk g hg x<GOAL>{a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a | f a < g a} x
<VAR>θ : ℝ<VAR>k : ℤ<GOAL>(↑θ).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
<VAR>θ : ℝ<VAR>k : ℤ<GOAL>-π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : InvolutiveInv α<VAR>f g : Filter α<VAR>s : Set α<GOAL>f⁻¹ ≤ g ↔ f ≤ g⁻¹
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>n : ℕ<GOAL>Integrable (martingalePart f ℱ μ n) μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>hf_int : ∀ (n : ℕ), Integrable (f n) μ<VAR>n : ℕ<GOAL>Integrable ((fun n => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])) n) μ
<VAR>R S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : EssFiniteType R S<GOAL>FormallyUnramified R S ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1
<VAR>R S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : EssFiniteType R S<GOAL>(∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = Submodule.span (S ⊗[R] S) {e}) ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1
<VAR>R S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : EssFiniteType R S<VAR>this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S<GOAL>(∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = Submodule.span (S ⊗[R] S) {e}) ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1
<VAR>R S : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : EssFiniteType R S<VAR>this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S<GOAL>(∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {e}) ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
<VAR>α : Type u_1<VAR>I✝ B X : Set α<VAR>inst✝ : DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<VAR>I : Finset α<GOAL>(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I
<VAR>α : Type u_1<VAR>I✝ B X : Set α<VAR>inst✝ : DecidableEq α<VAR>E : Set α<VAR>Indep : Finset α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E<VAR>I : Finset α<GOAL>(∀ J ⊆ I, Indep J) ↔ Indep I
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<GOAL>Continuous (stdSimplexEquivIcc ℝ).invFun
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<GOAL>Continuous fun x => ![↑x, 1 - ↑x]
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a : M₀<VAR>h : IsUnit (Ring.inverse a)<GOAL>IsUnit a
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a : M₀<VAR>h : IsUnit (Ring.inverse a)<VAR>h✝ : Subsingleton M₀<GOAL>IsUnit a
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a : M₀<VAR>h : IsUnit (Ring.inverse a)<VAR>h✝ : Nontrivial M₀<GOAL>IsUnit a
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x → q x<VAR>x y : { x // p x }<GOAL>(fun x => ⟨↑x, ⋯⟩) x = (fun x => ⟨↑x, ⋯⟩) y → x = y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : StarRing R<VAR>inst✝⁶ : TrivialStar R<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : StarAddMonoid A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : ContinuousStar A<VAR>r : R<VAR>a : A<GOAL>{ toFun := __src✝.toFun, map_add' := ⋯ }.toFun (r • a) = (starRingEnd R) r • { toFun := __src✝.toFun, map_add' := ⋯ }.toFun a
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>S S' : Set (HeightOneSpectrum R)<VAR>n : ℕ<VAR>inst✝ : Fact (0 < n)<GOAL>Function.Injective ⇑fromUnitLift
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>S S' : Set (HeightOneSpectrum R)<VAR>n : ℕ<VAR>inst✝ : Fact (0 < n)<GOAL>Function.Injective (⇑(QuotientGroup.kerLift fromUnit) ∘ ⇑(QuotientGroup.quotientMulEquivOfEq ⋯).symm)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<GOAL>Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p ∧ p < ⊤<VAR>f : (i : α) → E i<GOAL>Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal