ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : IsClosed s<VAR>hs : s.Nonempty<GOAL>x ∉ s ↔ 0 < Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : x ∉ closure s<GOAL>ContinuousAt (fun x => (Metric.infDist x s)⁻¹) x
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>t : Set α<VAR>x : α<VAR>Φ : α → β<VAR>hΦ : Isometry Φ<GOAL>Metric.infDist (Φ x) (Φ '' t) = Metric.infDist x t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>h : y ∈ s<GOAL>Metric.infDist x (s ∩ Metric.closedBall x (dist y x)) = Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : IsCompact s<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ s, Metric.infDist x s = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>h : IsClosed s<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ s, Metric.infDist x s = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ closure s, Metric.infDist x s = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>↑(Metric.infNndist x s) = Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>LipschitzWith 1 fun x => Metric.infNndist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>UniformContinuous fun x => Metric.infNndist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Continuous fun x => Metric.infNndist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<GOAL>0 ≤ Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<GOAL>EMetric.hausdorffEdist s t ≠ ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Metric.hausdorffDist s s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<GOAL>Metric.hausdorffDist s t = Metric.hausdorffDist t s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Metric.hausdorffDist s ∅ = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Metric.hausdorffDist ∅ s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, Metric.infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, Metric.infDist x s ≤ r<GOAL>Metric.hausdorffDist s t ≤ r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r<GOAL>Metric.hausdorffDist s t ≤ r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>hs : s.Nonempty<VAR>bs : Bornology.IsBounded s<VAR>ht : t.Nonempty<VAR>bt : Bornology.IsBounded t<GOAL>Metric.hausdorffDist s t ≤ Metric.diam (s ∪ t)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>Metric.infDist x t ≤ Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>x : α<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : Metric.hausdorffDist s t < r<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>∃ y ∈ t, dist x y < r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>y : α<VAR>r : ℝ<VAR>h : y ∈ t<VAR>H : Metric.hausdorffDist s t < r<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>∃ x ∈ s, dist x y < r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>x : α<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>Metric.infDist x t ≤ Metric.infDist x s + Metric.hausdorffDist s t
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>s t : Set α<VAR>Φ : α → β<VAR>h : Isometry Φ<GOAL>Metric.hausdorffDist (Φ '' s) (Φ '' t) = Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t u : Set α<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t u : Set α<VAR>fin : EMetric.hausdorffEdist t u ≠ ⊤<GOAL>Metric.hausdorffDist s u ≤ Metric.hausdorffDist s t + Metric.hausdorffDist t u
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Metric.hausdorffDist s (closure s) = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<GOAL>Metric.hausdorffDist (closure s) t = Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<GOAL>Metric.hausdorffDist s (closure t) = Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<GOAL>Metric.hausdorffDist (closure s) (closure t) = Metric.hausdorffDist s t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>Metric.hausdorffDist s t = 0 ↔ closure s = closure t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>Metric.hausdorffDist s t = 0 ↔ s = t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : PartitionOfUnity ι X s<GOAL>LocallyFinite fun i => Function.support ⇑(self.toFun i)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : PartitionOfUnity ι X s<VAR>x : X<GOAL>∑ᶠ (i : ι), (self.toFun i) x ≤ 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : PartitionOfUnity ι X s<VAR>x : X<GOAL>x ∈ s → ∑ᶠ (i : ι), (self.toFun i) x = 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : PartitionOfUnity ι X s<GOAL>0 ≤ self.toFun
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : BumpCovering ι X s<GOAL>0 ≤ self.toFun
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : BumpCovering ι X s<GOAL>LocallyFinite fun i => Function.support ⇑(self.toFun i)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : BumpCovering ι X s<VAR>x : X<GOAL>x ∈ s → ∃ i, ⇑(self.toFun i) =ᶠ[𝓝 x] 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>s : optParam (Set X) Set.univ<VAR>self : BumpCovering ι X s<GOAL>self.toFun ≤ 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<GOAL>LocallyFinite fun i => Function.support ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<GOAL>LocallyFinite fun i => tsupport ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>i : ι<VAR>x : X<GOAL>0 ≤ (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∑ᶠ (i : ι), (f i) x = 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ i, 0 < (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<GOAL>∑ᶠ (i : ι), (f i) x ≤ 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<GOAL>0 ≤ ∑ᶠ (i : ι), (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>i : ι<VAR>x : X<GOAL>(f i) x ≤ 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>i : ι<GOAL>i ∈ ρ.finsupport x₀ ↔ i ∈ Function.support fun i => (ρ i) x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>↑(ρ.finsupport x₀) = Function.support fun i => (ρ i) x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>hx₀ : x₀ ∈ s<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>hx₀ : x₀ ∈ s<VAR>I : Finset ι<VAR>hI : ρ.finsupport x₀ ⊆ I<GOAL>∑ i ∈ I, (ρ i) x₀ = 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℝ M<VAR>φ : ι → X → M<GOAL>∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>{i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>i : ι<GOAL>i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport ⇑(ρ i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>ρ.finsupport x₀ ⊆ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∀ᶠ (y : X) in 𝓝 x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>E : Type u_1<VAR>AddCommMonoid E<VAR>SMulWithZero ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>g : X → E<VAR>i : ι<VAR>hg : ∀ x ∈ tsupport ⇑(f i), ContinuousAt g x<GOAL>Continuous fun x => (f i) x • g x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>E : Type u_1<VAR>AddCommMonoid E<VAR>SMulWithZero ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>ContinuousAdd E<VAR>g : ι → X → E<VAR>hg : ∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContinuousAt (g i) x<GOAL>Continuous fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (Function.support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>ρ : PartitionOfUnity ι X<VAR>x₀ : X<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (Function.support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>U : ι → Set X<VAR>hso : f.IsSubordinate U<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>x : X<GOAL>∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun x => (f x) z) ⊆ ↑is
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>E : Type u_1<VAR>AddCommMonoid E<VAR>SMulWithZero ℝ E<VAR>TopologicalSpace E<VAR>ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>ContinuousAdd E<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : f.IsSubordinate U<VAR>g : ι → X → E<VAR>hg : ∀ (i : ι), ContinuousOn (g i) (U i)<GOAL>Continuous fun x => ∑ᶠ (i : ι), (f i) x • g i x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<GOAL>LocallyFinite fun i => Function.support ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<GOAL>LocallyFinite fun i => tsupport ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<GOAL>{i | (f i) x ≠ 0}.Finite
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>0 ≤ (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>(f i) x ≤ 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>i : ι<VAR>s : Set X<GOAL>⇑(BumpCovering.single i s) = Pi.single i 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>U V : ι → Set X<VAR>hU : f.IsSubordinate U<VAR>hV : ∀ (i : ι), U i ⊆ V i<GOAL>f.IsSubordinate V
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NormalSpace X<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NormalSpace X<VAR>ParacompactSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NormalSpace X<VAR>ParacompactSpace X<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<VAR>hx : x ∈ s<GOAL>⇑(f (f.ind x hx)) =ᶠ[𝓝 x] 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<VAR>hx : x ∈ s<GOAL>(f (f.ind x hx)) x = 1
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>h : (f i) x = 0<GOAL>f.toPOUFun i x = 0
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>Function.support (f.toPOUFun i) ⊆ Function.support ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<GOAL>f.toPOUFun i x = (f i) x * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>∃ t, f.toPOUFun i =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - f j))
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>Continuous (f.toPOUFun i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>(f.toPartitionOfUnity i) x = (f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<GOAL>(f.toPartitionOfUnity i) x = (f i) x * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<GOAL>∃ t, ⇑(f.toPartitionOfUnity i) =ᶠ[𝓝 x] ⇑(f i) * ⇑(∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - f j))
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>h : (f i) x = 0<GOAL>(f.toPartitionOfUnity i) x = 0
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<GOAL>Function.support ⇑(f.toPartitionOfUnity i) ⊆ Function.support ⇑(f i)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<GOAL>∑ᶠ (i : ι), (f.toPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>U : ι → Set X<VAR>h : f.IsSubordinate U<GOAL>f.toPartitionOfUnity.IsSubordinate U
<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>e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜₁ F₁ E₁<VAR>VectorBundle 𝕜₂ F₂ E₂<VAR>MemTrivializationAtlas e₁<VAR>MemTrivializationAtlas e₁'<VAR>MemTrivializationAtlas e₂<VAR>MemTrivializationAtlas e₂'<GOAL>ContinuousOn (Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<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>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>Trivialization.IsLinear 𝕜₁ e₁<VAR>Trivialization.IsLinear 𝕜₂ e₂<VAR>p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x<GOAL>↑(Pretrivialization.continuousLinearMap σ e₁ e₂) p = (p.proj, (Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj).comp (p.snd.comp (Trivialization.symmL 𝕜₁ e₁ p.proj)))
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<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>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>Trivialization.IsLinear 𝕜₁ e₁<VAR>Trivialization.IsLinear 𝕜₂ e₂<VAR>p : B × (F₁ →SL[σ] F₂)<GOAL>↑(Pretrivialization.continuousLinearMap σ e₁ e₂).symm p = { proj := p.1, snd := (Trivialization.symmL 𝕜₂ e₂ p.1).comp (p.2.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ p.1)) }
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<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>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>Trivialization.IsLinear 𝕜₁ e₁<VAR>Trivialization.IsLinear 𝕜₂ e₂<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet<VAR>L : F₁ →SL[σ] F₂<GOAL>(Pretrivialization.continuousLinearMap σ e₁ e₂).symm b L = (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))
<VAR>𝕜₁ : Type u_1<VAR>NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<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>e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>FiberBundle F₁ E₁<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₂ E₂<VAR>Trivialization.IsLinear 𝕜₁ e₁<VAR>Trivialization.IsLinear 𝕜₁ e₁'<VAR>Trivialization.IsLinear 𝕜₂ e₂<VAR>Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)<VAR>L : F₁ →SL[σ] F₂<GOAL>(Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L = (↑(Pretrivialization.continuousLinearMap σ e₁' e₂') { proj := b, snd := (Pretrivialization.continuousLinearMap σ e₁ e₂).symm b L }).2
<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>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<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>he₁ : MemTrivializationAtlas e₁<VAR>he₂ : MemTrivializationAtlas e₂<GOAL>(Trivialization.continuousLinearMap σ e₁ e₂).baseSet = e₁.baseSet ∩ e₂.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>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<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>he₁ : MemTrivializationAtlas e₁<VAR>he₂ : MemTrivializationAtlas e₂<VAR>p : Bundle.TotalSpace (F₁ →SL[σ] F₂) (Bundle.ContinuousLinearMap σ E₁ E₂)<GOAL>↑(Trivialization.continuousLinearMap σ e₁ e₂) p = (p.proj, (Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj).comp (ContinuousLinearMap.comp p.snd (Trivialization.symmL 𝕜₁ e₁ p.proj)))