ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<GOAL>ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<GOAL>ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<GOAL>ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<GOAL>MapsTo f₁ (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) (e₁.source ×ˢ e₂.source)
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<GOAL>EqOn (toFun' e₁ e₂) ((f₃ ∘ f₂) ∘ f₁) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<VAR>b : B<VAR>v₁ : E₁ b<VAR>v₂ : E₂ b<VAR>hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet<VAR>right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet<GOAL>toFun' e₁ e₂ { proj := b, snd := (v₁, v₂) } = ((f₃ ∘ f₂) ∘ f₁) { proj := b, snd := (v₁, v₂) }
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<VAR>b : B<VAR>v₁ : E₁ b<VAR>v₂ : E₂ b<VAR>hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet<VAR>right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet<GOAL>b = (↑e₁ { proj := b, snd := v₁ }).1
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<VAR>b : B<VAR>v₁ : E₁ b<VAR>v₂ : E₂ b<VAR>hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet<VAR>right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet<GOAL>{ proj := b, snd := v₁ } ∈ e₁.source
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<VAR>hf₁ : Continuous f₁<VAR>hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)<VAR>hf₃ : Continuous f₃<VAR>b : B<VAR>v₁ : E₁ b<VAR>v₂ : E₂ b<VAR>hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet<VAR>right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet<GOAL>{ proj := b, snd := v₁ }.proj ∈ e₁.baseSet
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>eι : ι ≃ ι'<GOAL>(e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>filter (fun x => decide (a = x)) l = replicate (count a l) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y = ⊥<GOAL>f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<GOAL>f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<GOAL>f x ≤ sSup (f '' Iio y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<GOAL>f y ∈ upperBounds (f '' Iio y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<GOAL>∀ a < y, f a ≤ f y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x : α<GOAL>dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁.diff (a :: l₂) = (l₁.diff l₂).erase a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>(l₁.diff l₂).erase a = l₁.diff (a :: l₂)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htn : ∀ (i : ι), (t i).Nonempty<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<GOAL>(⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htn : ∀ (i : ι), (t i).Nonempty<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<GOAL>(t i₀ ∩ ⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<VAR>htn : ∀ (i : ι), t i ≠ ∅<GOAL>t i₀ ∩ ⋂ i, t i ≠ ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<VAR>htn : ∀ (i : ι), t i ≠ ∅<GOAL>¬(Directed (fun x x_1 => x ⊇ x_1) t → ∃ i, t i₀ ∩ t i = ∅)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<VAR>htn : ∀ (i : ι), t i ≠ ∅<GOAL>Directed (fun x x_1 => x ⊇ x_1) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<VAR>htn : ∀ (i : ι), (t i).Nonempty<GOAL>Directed (fun x x_1 => x ⊇ x_1) t ∧ ∀ (i : ι), (t i₀ ∩ t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<VAR>i₀ : ι := hι.some<VAR>htn : ∀ (i : ι), (t i).Nonempty<VAR>i j : ι<VAR>hji₀ : t i₀ ⊇ t j<VAR>hji : t i ⊇ t j<GOAL>(t i₀ ∩ t i).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet sᶜ<VAR>f g : α →ₛ β<GOAL>↑(piecewise sᶜ hs f g) = ↑(piecewise s ⋯ g f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝² : (i : ι) → DecidableEq (γ i)<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → Zero (γ i)<VAR>x : (i : ι) → β i<GOAL>hammingDist 0 x = hammingNorm x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun a b => a ∉ closure {b} ∨ b ∉ closure {a}
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>inst✝¹ : l₁.NeBot<VAR>inst✝ : l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>he₁ : f ≤ᶠ[l₁] g<VAR>he₂ : g ≤ᶠ[l₂] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>inst✝¹ : l₁.NeBot<VAR>inst✝ : l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : Continuous (s.restrict f)<VAR>hg : Continuous (s.restrict g)<VAR>he₁ : f ≤ᶠ[l₁] g<VAR>he₂ : g ≤ᶠ[l₂] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>l₁ l₂ : Filter X<VAR>inst✝¹ : l₁.NeBot<VAR>inst✝ : l₂.NeBot<VAR>hl₁ : l₁ ≤ 𝓟 s<VAR>hl₂ : l₂ ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : Continuous (s.restrict f)<VAR>hg : Continuous (s.restrict g)<VAR>he₁ : f ≤ᶠ[l₁] g<VAR>he₂ : g ≤ᶠ[l₂] f<VAR>b : ↑s<VAR>h : s.restrict f b = s.restrict g b<GOAL>∃ x ∈ s, f x = g x
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>mF : MeasurableSpace F<VAR>Y : α → F<VAR>hY : Measurable Y<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>∫ (x : α), (μ[A.indicator fun x => 1|MeasurableSpace.comap Y mF]) x ∂μ = (μ A).toReal
<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>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid N₂<VAR>inst✝¹⁴ : Module R N₂<VAR>inst✝¹³ : Semiring R₁<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : SMulCommClass R R N₂<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring S₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>M : Matrix n m N₂<VAR>x : n → R₁<VAR>y : m → R₂<GOAL>(((toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i : n, ∑ j : m, σ₁ (x i) •> σ₂ (y j) •> M i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid N₂<VAR>inst✝¹⁴ : Module R N₂<VAR>inst✝¹³ : Semiring R₁<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : SMulCommClass R R N₂<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring S₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>M : Matrix n m N₂<VAR>x : n → R₁<VAR>y : m → R₂<GOAL>∑ i : n, ∑ j : m, σ₂ (y j) •> σ₁ (x i) •> M i j = ∑ i : n, ∑ j : m, σ₁ (x i) •> σ₂ (y j) •> M i j
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<GOAL>index K V ≤ index K' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K' V<GOAL>index K V ≤ index K' V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K' V<GOAL>index K' V ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K K' V : Set G<VAR>hK' : IsCompact K'<VAR>h : K ⊆ K'<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K' ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K' V<GOAL>∃ x ∈ {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = index K' V
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x✝ y✝ : M<VAR>f : N →* M<VAR>x y : N<GOAL>c (f x) (f y) ↔ c.mk' (f x) = c.mk' (f y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x✝ y✝ : M<VAR>f : N →* M<VAR>x y : N<GOAL>↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝¹ y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>ε : ℝ<VAR>x x✝ : α<GOAL>x✝ ∈ UniformSpace.ball x {p | dist p.1 p.2 < ε} ↔ x✝ ∈ ball x ε
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>b₁ : B.IsRefl<VAR>W : Submodule K V<GOAL>finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>b₁ : B.IsRefl<VAR>W : Submodule K V<GOAL>finrank K ↥W + finrank K ↥(range (domRestrict B W)).dualCoannihilator = finrank K V + finrank K ↥(ker (domRestrict B W))
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>hd : HasFDerivAt d d' x<GOAL>HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x