ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑X.toTopCat<GOAL>(Opens.map f.val.base).op.obj (op ((opensFunctor f).obj U)) = op U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>S✝ S : ConvexCone 𝕜 E<GOAL>S.Blunt → S.Salient
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>S✝ S : ConvexCone 𝕜 E<GOAL>¬S.Pointed → ¬S.Flat
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>c : CharacterModule (A ⊗[R] B)<VAR>r : R<VAR>a : A<VAR>x✝ : B<GOAL>({ toFun := fun x => AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯ }.toFun (r • a)) x✝ = ((RingHom.id R) r • { toFun := fun x => AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯ }.toFun a) x✝
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>r : R<VAR>c : CharacterModule (A ⊗[R] B)<VAR>x✝¹ : A<VAR>x✝ : B<GOAL>(({ toFun := fun c => { toFun := fun x => AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (r • c)) x✝¹) x✝ = (((RingHom.id R) r • { toFun := fun c => { toFun := fun x => AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun c) x✝¹) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<GOAL>card α = 0 ↔ IsEmpty α
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>k : n<VAR>d : α<VAR>a b : n<GOAL>(stdBasisMatrix i j c * stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>k : n<VAR>d : α<VAR>a b : n<GOAL>(∑ x : n, (if i = a ∧ j = x then c else 0) * if j = x ∧ k = b then d else 0) = if i = a ∧ k = b then c * d else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>x : α<VAR>inst✝ : MeasurableSingletonClass α<GOAL>IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>x : α<VAR>inst✝ : MeasurableSingletonClass α<VAR>this : f =ᶠ[ae (μ.restrict {x})] fun x_1 => f x<GOAL>IntegrableOn f {x} μ ↔ f x = 0 ∨ μ {x} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>x : α<VAR>inst✝ : MeasurableSingletonClass α<VAR>this : f =ᶠ[ae (μ.restrict {x})] fun x_1 => f x<GOAL>f x = 0 ∨ (μ.restrict {x}) univ < ⊤ ↔ f x = 0 ∨ μ {x} < ⊤
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<GOAL>x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : Dense s<VAR>t : Set X<VAR>ht : t.Finite<GOAL>Dense (s \ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : Dense s<VAR>t : Set X<VAR>ht : t.Finite<GOAL>t = ↑ht.toFinset
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal - ↑(-f a).toNNReal ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (fun a => ↑(-f a).toNNReal) μ
<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>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(cons h p).IsPath → p.IsPath
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<GOAL>x = 0 ∧ y = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<VAR>ha : ↑a ≠ 0<GOAL>x = 0 ∧ y = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<VAR>ha : ↑a ≠ 0<VAR>hf : ¬(x = 0 ∧ y = 0)<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<VAR>ha : ↑a ≠ 0<VAR>hf : ¬(x = 0 ∧ y = 0)<VAR>hx : ¬x = 0<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : legendreSym p a = -1<VAR>x y : ZMod p<VAR>hxy : x ^ 2 - ↑a * y ^ 2 = 0<VAR>ha : ↑a ≠ 0<VAR>hf : ¬(x = 0 ∧ y = 0)<VAR>hy : ¬y = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<GOAL>prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>a✝ : Path a₁ a₂<VAR>b✝ : Path b₁ b₂<GOAL>prod ⟦a✝⟧ ⟦b✝⟧ ⬝ prod r₁ r₂ = prod (⟦a✝⟧ ⬝ r₁) (⟦b✝⟧ ⬝ r₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>a✝¹ : Path a₁ a₂<VAR>b✝¹ : Path b₁ b₂<VAR>a✝ : Path a₂ a₃<VAR>b✝ : Path b₂ b₃<GOAL>prod ⟦a✝¹⟧ ⟦b✝¹⟧ ⬝ prod ⟦a✝⟧ ⟦b✝⟧ = prod (⟦a✝¹⟧ ⬝ ⟦a✝⟧) (⟦b✝¹⟧ ⬝ ⟦b✝⟧)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<GOAL>∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>s1 s2 : Set (Set Ω)<VAR>μ : Measure Ω<GOAL>IndepSets s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>(∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s✝ s : Finset α<GOAL>(map (Embedding.subtype fun x => x ∈ s) s.attach).val = s.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s✝ s : Finset α<GOAL>Multiset.map (⇑(Embedding.subtype fun x => x ∈ s)) s.val.attach = s.val
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set M<GOAL>span R s = LinearMap.range (Finsupp.total (↑s) M R Subtype.val)
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : x < 1<VAR>hz : 0 < z<GOAL>x ^ z < 1
<VAR>z : ℝ<VAR>hz : 0 < z<VAR>x : ℝ≥0<VAR>hx : ↑x < 1<GOAL>↑x ^ z < 1
<VAR>z : ℝ<VAR>hz : 0 < z<VAR>x : ℝ≥0<VAR>hx : x < 1<GOAL>↑x ^ z < 1
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>a : α<VAR>l : List α<VAR>s : Stream' α<GOAL>map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<GOAL>BddBelow (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<VAR>x : PGame<VAR>hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))<GOAL>BddBelow (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Game<VAR>x : PGame<VAR>hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))<VAR>i : ι<GOAL>⟦x⟧ ≤ f i
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b c : α<VAR>inst✝ : Invertible c<GOAL>c * a = b ↔ a = ⅟c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : f.LimZero<GOAL>(-f).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : f.LimZero<GOAL>(-1 * f).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>1 ≤ s.encard ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>ha : a ≤ c<VAR>hb : b ≤ c<GOAL>a ∉ Ι b c → b ∉ Ι a c → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>ha : a ≤ c<VAR>hb : b ≤ c<GOAL>a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a → b ≤ a ∧ b ≤ c ∨ c < b ∧ a < b → a = b
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) = ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) + ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) = ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ + (shortComplexFunctor C c i).map ψ)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧ ContDiffWithinAtProp I 𝓘(𝕜, E') n (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ (ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x) ∧ ContDiffWithinAtProp I 𝓘(𝕜, E') n (↑(chartAt E' ((↑(extChartAt I' (f x)) ∘ f) x)) ∘ (↑(extChartAt I' (f x)) ∘ f) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (↑(extChartAt I' (f x)) ∘ f) s x ↔ ContinuousWithinAt f s x<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x)) ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n ((((↑I' ∘ ↑(chartAt H' (f x))) ∘ f) ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : a ∈ frontier s<GOAL>a.IsLimit
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<GOAL>a.IsLimit
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<VAR>h : ¬a.IsLimit<GOAL>False
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>ha : (∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ s).Nonempty) ∧ ∀ (o : Set Ordinal.{u}), IsOpen o → a ∈ o → (o ∩ sᶜ).Nonempty<VAR>h : IsOpen {a}<GOAL>False