ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ι<GOAL>MeasurableSet {ω | (fun ω => max (τ ω) (π ω)) ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ι<GOAL>MeasurableSet ({a | τ a ≤ i} ∩ {a | π a ≤ i})
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s✝ : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x : V<VAR>hx : x ≠ 0<GOAL>angle x (-x) = π
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X✝ Y : Set α<VAR>M M' : Matroid α<VAR>X : Set α<GOAL>M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I✝ J X✝ Y : Set α<VAR>M M' : Matroid α<VAR>X : Set α<VAR>h : M ↾ X = M' ↾ X<VAR>I : Set α<VAR>hIX : I ⊆ X<GOAL>M.Indep I ↔ M'.Indep I
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I✝ J X✝ Y : Set α<VAR>M M' : Matroid α<VAR>X : Set α<VAR>h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I<VAR>I : Set α<VAR>hI : I ⊆ X<GOAL>(M ↾ X).Indep I ↔ (M' ↾ X).Indep I
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<GOAL>P ∉ R[X]⁰ ↔ ∃ a, a ≠ 0 ∧ a • P = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>hP : P ∉ R[X]⁰<GOAL>∃ a, a ≠ 0 ∧ a • P = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>hP : P ∉ R[X]⁰<VAR>h : ∀ (a : R), a ≠ 0 → a • P ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a p P : R[X]<VAR>hP : P ∉ R[X]⁰<VAR>h : ∀ (a : R), a ≠ 0 → a • P ≠ 0<VAR>Q : R[X]<VAR>hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a✝ p P : R[X]<VAR>hP : P ∉ R[X]⁰<VAR>h : ∀ (a : R), a ≠ 0 → a • P ≠ 0<VAR>Q : R[X]<VAR>hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}<VAR>a : R<VAR>ha : a • P = 0<GOAL>a = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>a✝ p P : R[X]<VAR>hP : P ∉ R[X]⁰<VAR>h : ∀ (a : R), a ≠ 0 → a • P ≠ 0<VAR>Q : R[X]<VAR>hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}<VAR>a : R<VAR>ha : a ≠ 0<GOAL>a • P ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<GOAL>‖f‖ = a
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<VAR>x : E<VAR>hx : x ≠ 0<GOAL>‖f‖ = a
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<VAR>x : E<VAR>hx : 0 < ‖x‖<GOAL>‖f‖ = a
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<VAR>x : E<VAR>hx : 0 < ‖x‖<VAR>ha : 0 ≤ a<GOAL>‖f‖ = a
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<VAR>x : E<VAR>hx : 0 < ‖x‖<VAR>ha : 0 ≤ a<GOAL>a ≤ ‖f‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>l : AssocList α β<GOAL>findEntryP? p l = List.find? (fun x => match x with | (a, b) => p a b) l.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Bool<VAR>key✝ : α<VAR>value✝ : β<VAR>tail✝ : AssocList α β<VAR>tail_ih✝ : findEntryP? p tail✝ = List.find? (fun x => match x with | (a, b) => p a b) tail✝.toList<GOAL>(bif p key✝ value✝ then some (key✝, value✝) else findEntryP? p tail✝) = match p key✝ value✝ with | true => some (key✝, value✝) | false => List.find? (fun x => p x.fst x.snd) tail✝.toList
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>hausdorffDist s ∅ = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : s = ∅<GOAL>hausdorffDist s ∅ = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : s.Nonempty<GOAL>hausdorffDist s ∅ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<VAR>this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<VAR>this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)<VAR>φ₀ : E →ₗ[𝕜] E × F := id.prod g<VAR>this : LeftInverse Prod.fst ⇑φ₀<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<VAR>this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)<VAR>φ₀ : E →ₗ[𝕜] E × F := id.prod g<VAR>this : LeftInverse Prod.fst ⇑φ₀<VAR>φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<VAR>this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)<VAR>φ₀ : E →ₗ[𝕜] E × F := id.prod g<VAR>this : LeftInverse Prod.fst ⇑φ₀<VAR>φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯<VAR>ψ : ↥g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous ⋯<GOAL>Continuous ⇑g
<VAR>θ : Angle<GOAL>θ.toReal = -π / 2 ↔ θ = ↑(-π / 2)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>i : Fin n<GOAL>b.flag i.castSucc ⋖ b.flag i.succ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>i : Fin n<GOAL>b.flag i.castSucc ⋖ span K {b i} ⊔ b.flag i.castSucc
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>n : ℕ<VAR>b : Basis (Fin n) K V<VAR>i : Fin n<GOAL>b i ∉ b.flag i.castSucc
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<GOAL>Convex ℝ (Metric.cthickening δ s)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<VAR>hδ : 0 ≤ δ<GOAL>Convex ℝ (Metric.cthickening δ s)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<VAR>hδ : δ ≤ 0<GOAL>Convex ℝ (Metric.cthickening δ s)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<GOAL>∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x : X<VAR>hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V<VAR>hxS : x ∈ S<GOAL>∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x : X<VAR>hx : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ V<VAR>hxS : x ∈ S<GOAL>∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x : X<VAR>hxS : x ∈ S<VAR>hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V<GOAL>∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (eval x₀ ∘ u)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x : X<VAR>hxS : x ∈ S<VAR>hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V<GOAL>Continuous fun f => u f x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α →𝒄 Part β<VAR>g : α →𝒄 β → Part γ<VAR>c : Chain α<GOAL>((↑f).partBind g.toOrderHom) (ωSup c) = ωSup (c.map ((↑f).partBind g.toOrderHom))
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α →𝒄 Part β<VAR>g : α →𝒄 β → Part γ<VAR>c : Chain α<GOAL>((↑f).partBind ↑g) (ωSup c) = f (ωSup c) >>= g (ωSup c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<VAR>e : α ≃ β<VAR>x : Sym α n<GOAL>map (⇑e.symm) (map (⇑e) x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<VAR>e : α ≃ β<VAR>x : Sym β n<GOAL>map (⇑e) (map (⇑e.symm) x) = x
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ∃ r, 0 < r ∧ r • x = y<GOAL>SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>r : R<VAR>hr : 0 < r<VAR>hy : r • x ≠ 0<GOAL>SameRay R x (r • x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n a : ℕ), ∃ b > a, P n b<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → ℕ → Prop<VAR>u : ℕ → ℕ → ℕ<VAR>hu : ∀ (n a : ℕ), u n a > a<VAR>hu' : ∀ (n a : ℕ), P n (u n a)<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → ℕ → Prop<VAR>u : ℕ → ℕ → ℕ<VAR>hu : ∀ (n a : ℕ), u n a > a<VAR>hu' : ∀ (n a : ℕ), P n (u n a)<GOAL>(StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) ∧ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v => u (n + 1) v)
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>a < 2 ^ a
<VAR>α✝ β α : Type u<GOAL>#α < 2 ^ #α
<VAR>α✝ β α : Type u<GOAL>#α < #(Set α)
<VAR>α✝ β α : Type u<GOAL>¬Quotient.liftOn₂ (#(Set α)) (#α) (fun α β => Nonempty (α ↪ β)) instLE.proof_1
<VAR>α✝ β α : Type u<VAR>f : Set α → α<VAR>hf : Injective f<GOAL>False
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : CanonicallyOrderedAddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>a✝ : ι → μ<GOAL>a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<GOAL>pkg.compare pkg' ∘ pkg'.compare pkg = id
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>uc : UniformContinuous (pkg.compare pkg')<GOAL>pkg.compare pkg' ∘ pkg'.compare pkg = id
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>uc : UniformContinuous (pkg.compare pkg')<VAR>uc' : UniformContinuous (pkg'.compare pkg)<GOAL>pkg.compare pkg' ∘ pkg'.compare pkg = id
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>uc : UniformContinuous (pkg.compare pkg')<VAR>uc' : UniformContinuous (pkg'.compare pkg)<GOAL>∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>uc : UniformContinuous (pkg.compare pkg')<VAR>uc' : UniformContinuous (pkg'.compare pkg)<VAR>a : α<GOAL>(pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>uc : UniformContinuous (pkg.compare pkg')<VAR>uc' : UniformContinuous (pkg'.compare pkg)<VAR>a : α<GOAL>pkg'.coe a = id (pkg'.coe a)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>Eₘ[s, t] = ∑ a ∈ s * t, (filter (fun x => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)).card = ∑ x ∈ s * t, (filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)).card