ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜₁ (E₁ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜₂ (E₂ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜₁ F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜₂ F₂ E₂<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)<VAR>x₀ : B<VAR>x : Bundle.TotalSpace (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)<GOAL>↑(trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀) x = (x.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ x₀ x.proj x₀ x.proj x.snd)
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜₁ (E₁ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜₂ (E₂ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜₁ F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜₂ F₂ E₂<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)<VAR>x₀ : B<GOAL>(trivializationAt (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂) x₀).source = Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜₁ (E₁ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜₂ (E₂ x)<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜₁ F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜₂ F₂ E₂<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)<VAR>x₀ : B<GOAL>(trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀).target = ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X ⊕ Y<GOAL>Metric.glueDist Φ Ψ ε x x = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>p : Z<GOAL>Metric.glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x y : X ⊕ Y<GOAL>Metric.glueDist Φ Ψ ε x y = Metric.glueDist Φ Ψ ε y x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x y : X ⊕ Y<GOAL>Metric.glueDist Ψ Φ ε x.swap y.swap = Metric.glueDist Φ Ψ ε x y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y : Y<GOAL>ε ≤ Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : Y<VAR>y : X<GOAL>ε ≤ Metric.glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y z : Y<GOAL>Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤ Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + Metric.glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<GOAL>Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤ Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + Metric.glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x y z : X ⊕ Y<GOAL>Metric.glueDist Φ Ψ ε x z ≤ Metric.glueDist Φ Ψ ε x y + Metric.glueDist Φ Ψ ε y z
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>p q : X ⊕ Y<GOAL>Metric.glueDist Φ Ψ ε p q = 0 → p = q
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>s : Set ((X ⊕ Y) × (X ⊕ Y))<GOAL>s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), Metric.glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>p q : X ⊕ Y<VAR>x : X<VAR>y : Y<GOAL>Metric.Sum.dist p q = Metric.glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 p q
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>x y : X ⊕ Y<GOAL>Metric.Sum.dist x y = Metric.Sum.dist y x
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>x : X<VAR>y : Y<GOAL>1 ≤ Metric.Sum.dist (Sum.inl x) (Sum.inr y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>x : X<VAR>y : Y<GOAL>1 ≤ Metric.Sum.dist (Sum.inr y) (Sum.inl x)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>s : Set ((X ⊕ Y) × (X ⊕ Y))<GOAL>s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε > 0, ∀ (a b : X ⊕ Y), Metric.Sum.dist a b < ε → (a, b) ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>x y : X ⊕ Y<GOAL>dist x y = Metric.Sum.dist x y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<GOAL>Isometry Sum.inl
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<GOAL>Isometry Sum.inr
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>i : ι<VAR>x y : E i<GOAL>dist ⟨i, x⟩ ⟨i, y⟩ = dist x y
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>i j : ι<VAR>h : i ≠ j<VAR>x : E i<VAR>y : E j<GOAL>dist ⟨i, x⟩ ⟨j, y⟩ = dist x ⋯.some + 1 + dist ⋯.some y
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>i j : ι<VAR>h : i ≠ j<VAR>x : E i<VAR>y : E j<GOAL>1 ≤ dist ⟨i, x⟩ ⟨j, y⟩
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>x y : (i : ι) × E i<VAR>h : dist x y < 1<GOAL>x.fst = y.fst
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>x y z : (i : ι) × E i<GOAL>dist x z ≤ dist x y + dist y z
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>s : Set ((i : ι) × E i)<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>i : ι<GOAL>Isometry (Sigma.mk i)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>(i : ι) → MetricSpace (E i)<VAR>∀ (i : ι), CompleteSpace (E i)<GOAL>CompleteSpace ((i : ι) × E i)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Nonempty Z<VAR>MetricSpace Z<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<GOAL>Metric.toGlueL hΦ hΨ ∘ Φ = Metric.toGlueR hΦ hΨ ∘ Ψ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Nonempty Z<VAR>MetricSpace Z<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<GOAL>Isometry (Metric.toGlueL hΦ hΨ)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Nonempty Z<VAR>MetricSpace Z<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>hΦ : Isometry Φ<VAR>hΨ : Isometry Ψ<GOAL>Isometry (Metric.toGlueR hΦ hΨ)
<VAR>X : ℕ → Type u<VAR>(n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>x y : (n : ℕ) × X n<VAR>m : ℕ<VAR>hx : x.fst ≤ m<VAR>hy : y.fst ≤ m<GOAL>Metric.inductiveLimitDist f x y = dist (Nat.leRecOn hx (fun {k} => f k) x.snd) (Nat.leRecOn hy (fun {k} => f k) y.snd)
<VAR>X : ℕ → Type u<VAR>(n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<GOAL>Isometry (Metric.toInductiveLimit I n)
<VAR>X : ℕ → Type u<VAR>(n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>n : ℕ<GOAL>Metric.toInductiveLimit I n.succ ∘ f n = Metric.toInductiveLimit I n
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : CocompactMap α β<GOAL>Filter.Tendsto self.toFun (Filter.cocompact α) (Filter.cocompact β)
<VAR>F : Type u_1<VAR>α : outParam (Type u_2)<VAR>β : outParam (Type u_3)<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : CocompactMapClass F α β<VAR>f : F<GOAL>Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<GOAL>⇑f.toContinuousMap = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : CocompactMap α β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>h : Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)<GOAL>⇑{ toContinuousMap := f, cocompact_tendsto' := h } = ⇑f
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>⇑(CocompactMap.id α) = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : CocompactMap β γ<VAR>g : CocompactMap α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : CocompactMap β γ<VAR>g : CocompactMap α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>f : CocompactMap γ δ<VAR>g : CocompactMap β γ<VAR>h : CocompactMap α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<GOAL>(CocompactMap.id β).comp f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<GOAL>f.comp (CocompactMap.id α) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)<GOAL>Filter.Tendsto f (Filter.cocompact α) (Filter.cocompact β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : CocompactMap α β<VAR>s : Set β<VAR>hs : IsCompact s<VAR>h's : IsClosed s<GOAL>IsCompact (⇑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>T2Space β<VAR>f : CocompactMap α β<VAR>s : Set β<VAR>hs : IsCompact s<GOAL>IsCompact (⇑f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>a : α<GOAL>f.toCocompactMap a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>PartialOrder β<VAR>f g : C(α, β)<GOAL>f ≤ g ↔ ∀ (a : α), f a ≤ g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>PartialOrder β<VAR>f g : C(α, β)<GOAL>f < g ↔ (∀ (a : α), f a ≤ g a) ∧ ∃ a, f a < g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g : C(α, β)<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>f g : C(α, β)<VAR>a : α<GOAL>(f ⊔ g) a = f a ⊔ g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<VAR>a : α<GOAL>(s.sup' H f) a = s.sup' H fun i => (f i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<GOAL>⇑(s.sup' H f) = s.sup' H fun i => ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f g : C(α, β)<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>f g : C(α, β)<VAR>a : α<GOAL>(f ⊓ g) a = f a ⊓ g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<VAR>a : α<GOAL>(s.inf' H f) a = s.inf' H fun i => (f i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<GOAL>⇑(s.inf' H f) = s.inf' H fun i => ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : C(↑(Set.Icc a b), β)<GOAL>⇑(ContinuousMap.IccExtend h f) = Set.IccExtend h ⇑f
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : C(X, AddUnits M)<VAR>x : X<GOAL>↑(ContinuousMap.addUnitsLift f) x = ↑(f x)
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : C(X, Mˣ)<VAR>x : X<GOAL>↑(ContinuousMap.unitsLift f) x = ↑(f x)
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : C(X, M)ˣ<VAR>x : X<GOAL>↑((ContinuousMap.unitsLift.symm f) x) = ↑f x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : AddUnits C(X, M)<VAR>x : X<GOAL>↑((ContinuousMap.addUnitsLift.symm f) x) = ↑f x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : C(X, AddUnits M)<VAR>x : X<GOAL>↑(-ContinuousMap.addUnitsLift f) x = ↑(-f x)
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : C(X, Mˣ)<VAR>x : X<GOAL>↑(ContinuousMap.unitsLift f)⁻¹ x = ↑(f x)⁻¹
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : AddUnits C(X, M)<VAR>x : X<GOAL>↑(-(ContinuousMap.addUnitsLift.symm f) x) = ↑(-f) x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace X<VAR>Monoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : C(X, M)ˣ<VAR>x : X<GOAL>↑((ContinuousMap.unitsLift.symm f) x)⁻¹ = ↑f⁻¹ x
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<GOAL>Continuous fun x => ⋯.unit
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<VAR>x : X<GOAL>(ContinuousMap.unitsOfForallIsUnit h) x = ⋯.unit
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>NormedRing R<VAR>CompleteSpace R<VAR>f : C(X, R)<GOAL>IsUnit f ↔ ∀ (x : X), IsUnit (f x)
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>TopologicalSpace X<VAR>NormedDivisionRing R<VAR>CompleteSpace R<VAR>f : C(X, R)<GOAL>IsUnit f ↔ ∀ (x : X), f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>TopologicalSpace X<VAR>NormedField 𝕜<VAR>NormedDivisionRing R<VAR>Algebra 𝕜 R<VAR>CompleteSpace R<VAR>f : C(X, R)<GOAL>spectrum 𝕜 f = ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
<VAR>X : Type u_1<VAR>𝕜 : Type u_4<VAR>TopologicalSpace X<VAR>NormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>f : C(X, 𝕜)<GOAL>spectrum 𝕜 f = Set.range ⇑f
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>self : TopCat.PrelocalPredicate T<VAR>U V : TopologicalSpace.Opens ↑X<VAR>i : U ⟶ V<VAR>f : (x : ↥V) → T ↑x<GOAL>self.pred f → self.pred fun x => f ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>X T : TopCat<GOAL>∀ {x : TopologicalSpace.Opens ↑X} (f : ↥x → ↑T), (X.continuousPrelocal T).pred f = Continuous f
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>self : TopCat.LocalPredicate T<VAR>U : TopologicalSpace.Opens ↑X<VAR>f : (x : ↥U) → T ↑x<GOAL>(∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, self.pred fun x => f ((fun x => ⟨↑x, ⋯⟩) x)) → self.pred f
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.PrelocalPredicate T<VAR>U : TopologicalSpace.Opens ↑X<VAR>f : (x : ↥U) → T ↑x<VAR>h : P.pred f<GOAL>P.sheafify.pred f
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.PrelocalPredicate T<VAR>U V : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>f : { f // P.pred f }<VAR>x : ↥(Opposite.unop V)<GOAL>↑((TopCat.subpresheafToTypes P).map i f) x = ↑f ⟨↑x, ⋯⟩
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.PrelocalPredicate T<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(TopCat.subpresheafToTypes P).obj U = { f // P.pred f }
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.LocalPredicate T<GOAL>(TopCat.subpresheafToTypes P.toPrelocalPredicate).IsSheaf
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.LocalPredicate T<GOAL>(TopCat.subsheafToTypes P).val = TopCat.subpresheafToTypes P.toPrelocalPredicate
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.LocalPredicate T<VAR>U : TopologicalSpace.Opens ↑X<VAR>x : ↥U<VAR>f : (TopCat.subsheafToTypes P).presheaf.obj (Opposite.op U)<GOAL>TopCat.stalkToFiber P (↑x) ((TopCat.subsheafToTypes P).presheaf.germ x f) = ↑f x
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t<GOAL>Function.Surjective (TopCat.stalkToFiber P x)
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>P : TopCat.LocalPredicate T<VAR>x : ↑X<VAR>w : ∀ (U V : TopologicalSpace.OpenNhds x) (fU : (y : ↥U.obj) → T ↑y), P.pred fU → ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)<GOAL>Function.Injective (TopCat.stalkToFiber P x)
<VAR>X : Type u_1<VAR>t : TopologicalSpace X<GOAL>t = ⨅ u, TopologicalSpace.induced (fun x => x ∈ u) sierpinskiSpace
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Inducing ⇑(TopologicalSpace.productOfMemOpens X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<GOAL>Function.Injective ⇑(TopologicalSpace.productOfMemOpens X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<GOAL>Embedding ⇑(TopologicalSpace.productOfMemOpens X)
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<VAR>R : CategoryTheory.Presieve U<VAR>f : (V : TopologicalSpace.Opens ↑X) × { f // R f }<GOAL>TopCat.Presheaf.coveringOfPresieve U R f = f.fst
<VAR>X : TopCat<VAR>U : TopologicalSpace.Opens ↑X<VAR>R : CategoryTheory.Presieve U<VAR>hR : CategoryTheory.Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<GOAL>iSup (TopCat.Presheaf.coveringOfPresieve U R) = U
<VAR>X : TopCat<VAR>Y : TopologicalSpace.Opens ↑X<VAR>R : CategoryTheory.Presieve Y<GOAL>TopCat.Presheaf.presieveOfCoveringAux (TopCat.Presheaf.coveringOfPresieve Y R) Y = R
<VAR>X : TopCat<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCovering U) ∈ (Opens.grothendieckTopology ↑X).sieves (iSup U)
<VAR>X : TopCat<VAR>ι : Type v<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>f : (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }<GOAL>f.fst = U (TopCat.Presheaf.presieveOfCovering.indexOfHom U f)
<VAR>X : TopCat<VAR>ι : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} ι<VAR>B : ι ⥤ TopologicalSpace.Opens ↑X<GOAL>B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ TopologicalSpace.Opens.IsBasis (Set.range B.obj)
<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → TopologicalSpace.Opens ↑X<VAR>h : TopologicalSpace.Opens.IsBasis (Set.range B)<GOAL>(CategoryTheory.inducedFunctor B).IsCoverDense (Opens.grothendieckTopology ↑X)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<GOAL>CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>hf : IsOpenMap ⇑f<GOAL>CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) hf.functor
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>h : OpenEmbedding ⇑f<GOAL>⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>h : OpenEmbedding ⇑f<VAR>hF : F.IsSheaf<GOAL>TopCat.Presheaf.IsSheaf (⋯.functor.op ⋙ F)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑X) (TopologicalSpace.Opens.map f)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X) (TopologicalSpace.Opens.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → TopologicalSpace.Opens ↑X<VAR>F : TopCat.Presheaf C X<VAR>F' : TopCat.Sheaf C X<VAR>h : TopologicalSpace.Opens.IsBasis (Set.range B)<VAR>α : (CategoryTheory.inducedFunctor B).op ⋙ F ⟶ (CategoryTheory.inducedFunctor B).op ⋙ F'.val<VAR>i : ι<GOAL>((TopCat.Sheaf.restrictHomEquivHom F F' h) α).app (Opposite.op (B i)) = α.app (Opposite.op i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>ι : Type u_1<VAR>B : ι → TopologicalSpace.Opens ↑X<VAR>F : TopCat.Presheaf C X<VAR>F' : TopCat.Sheaf C X<VAR>h : TopologicalSpace.Opens.IsBasis (Set.range B)<VAR>α β : F ⟶ F'.val<VAR>he : ∀ (i : ι), α.app (Opposite.op (B i)) = β.app (Opposite.op (B i))<GOAL>α = β
<VAR>X : TopCat<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>(X : C) → MulOneClass ((CategoryTheory.forget C).obj X)<VAR>∀ (X Y : C), MonoidHomClass (X ⟶ Y) ((CategoryTheory.forget C).obj X) ((CategoryTheory.forget C).obj Y)<VAR>F : TopCat.Presheaf C X<VAR>self : F.SubmonoidPresheaf<VAR>U V : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>self.obj U ≤ Submonoid.comap (F.map i) (self.obj V)
<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>G : F.SubmonoidPresheaf<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>G.toLocalizationPresheaf.app U = CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U)))
<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>S : (x : ↑X) → Submonoid ↑(F.stalk x)<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(F.submonoidPresheafOfStalk S).obj U = ⨅ x, Submonoid.comap (F.germ x) (S ↑x)
<VAR>E : ℕ → Type u_2<VAR>x y : (n : ℕ) → E n<GOAL>PiNat.firstDiff x y = if h : x ≠ y then Nat.find ⋯ else 0
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>h : x ≠ y<GOAL>x (PiNat.firstDiff x y) ≠ y (PiNat.firstDiff x y)
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n < PiNat.firstDiff x y<GOAL>x n = y n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<GOAL>PiNat.firstDiff x y = PiNat.firstDiff y x