ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>EM : Type u_1<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_2<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>x : M<VAR>f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)<GOAL>IsUnit f ↔ f ∉ RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>EM : Type u_1<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_2<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>x : M<GOAL>nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>self : Path x y<GOAL>self.toFun 1 = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>self : Path x y<GOAL>self.toFun 0 = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ₁ γ₂ : Path x y<GOAL>⇑γ₁ = ⇑γ₂ → γ₁ = γ₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>f : ↑I → X<VAR>h₁ : Continuous f<VAR>h₂ : f 0 = x<VAR>h₃ : f 1 = y<GOAL>⇑{ toFun := f, continuous_toFun := h₁, source' := h₂, target' := h₃ } = f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Continuous ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ 0 = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ 1 = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>⇑γ.toContinuousMap = ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>⇑↑γ = ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>_t : ↑I<GOAL>(Path.refl x) _t = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a : X<GOAL>Set.range ⇑(Path.refl a) = {a}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>∀ (a : ↑I), γ.symm a = (⇑γ ∘ σ) a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ.symm.symm = γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Function.Bijective Path.symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a : X<GOAL>(Path.refl a).symm = Path.refl a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>Set.range ⇑γ.symm = Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Continuous fun p => p.1 p.2
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>Y : Type u_4<VAR>TopologicalSpace Y<VAR>f : Y → Path x y<VAR>g : Y → ↑I<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun y_1 => (f y_1) (g y_1)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>Y : Type u_4<VAR>TopologicalSpace Y<VAR>g : Y → Path x y<GOAL>Continuous ↿g ↔ Continuous g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>γ : Y → Path x y<VAR>f : Y → ℝ<VAR>hγ : Continuous ↿γ<VAR>hf : Continuous f<GOAL>Continuous fun t => (γ t).extend (f t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Continuous γ.extend
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>l r : Y → X<VAR>y : Y<VAR>l₁ : Filter ℝ<VAR>l₂ : Filter X<VAR>γ : (y : Y) → Path (l y) (r y)<VAR>hγ : Filter.Tendsto (↿γ) (𝓝 y ×ˢ Filter.map (Set.projIcc 0 1 ⋯) l₁) l₂<GOAL>Filter.Tendsto (↿fun x => (γ x).extend) (𝓝 y ×ˢ l₁) l₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : Y → ℝ<VAR>l r : Y → X<VAR>γ : (y : Y) → Path (l y) (r y)<VAR>y : Y<VAR>hγ : ContinuousAt (↿γ) (y, Set.projIcc 0 1 ⋯ (g y))<VAR>hg : ContinuousAt g y<GOAL>ContinuousAt (fun i => (γ i).extend (g i)) y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>ht : t ∈ Set.Icc 0 1<GOAL>γ.extend t = γ ⟨t, ht⟩
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ.extend 0 = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ.extend 1 = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ↑(Set.Icc 0 1)<GOAL>γ.extend ↑t = γ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>Set.range γ.extend = Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>ht : t ≤ 0<GOAL>γ.extend t = a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>ht : 1 ≤ t<GOAL>γ.extend t = b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a : X<GOAL>(Path.refl a).extend = fun x => a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>f : ℝ → X<VAR>hf : ContinuousOn f I<VAR>h₀ : f 0 = x<VAR>h₁ : f 1 = y<VAR>t : ↑I<GOAL>(Path.ofLine hf h₀ h₁) t ∈ f '' I
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<GOAL>(γ.trans γ') t = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>γ : Path x y<VAR>γ' : Path y z<GOAL>(γ.trans γ').symm = γ'.symm.trans γ.symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a : X<GOAL>(Path.refl a).trans (Path.refl a) = Path.refl a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b c : X<VAR>γ₁ : Path a b<VAR>γ₂ : Path b c<GOAL>Set.range ⇑(γ₁.trans γ₂) = Set.range ⇑γ₁ ∪ Set.range ⇑γ₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>γ : Path x y<VAR>f : X → Y<VAR>h : Continuous f<GOAL>⇑(γ.map h) = f ∘ ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>γ : Path x y<VAR>f : X → Y<VAR>h : Continuous f<GOAL>(γ.map h).symm = γ.symm.map h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y z : X<VAR>γ : Path x y<VAR>γ' : Path y z<VAR>f : X → Y<VAR>h : Continuous f<GOAL>(γ.trans γ').map h = (γ.map h).trans (γ'.map h)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ.map ⋯ = γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>γ : Path x y<VAR>Z : Type u_4<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>hf : Continuous f<VAR>g : Y → Z<VAR>hg : Continuous g<GOAL>(γ.map hf).map hg = γ.map ⋯
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a₁ a₂ b₁ b₂ : X<VAR>γ : Path a₂ b₂<VAR>ha : a₁ = a₂<VAR>hb : b₁ = b₂<GOAL>(γ.cast ha hb).symm = γ.symm.cast hb ha
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a₁ a₂ b₁ b₂ c₁ c₂ : X<VAR>γ : Path a₂ b₂<VAR>γ' : Path b₂ c₂<VAR>ha : a₁ = a₂<VAR>hb : b₁ = b₂<VAR>hc : c₁ = c₂<GOAL>(γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<VAR>x' y' : X<VAR>hx : x' = x<VAR>hy : y' = y<GOAL>⇑(γ.cast hx hy) = ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Type u_4<VAR>TopologicalSpace ι<VAR>a b : ι → X<VAR>γ : (t : ι) → Path (a t) (b t)<VAR>h : Continuous ↿γ<GOAL>Continuous ↿fun t => (γ t).symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Continuous Path.symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Type u_4<VAR>TopologicalSpace ι<VAR>a b : ι → X<VAR>γ : (t : ι) → Path (a t) (b t)<VAR>h : Continuous ↿γ<GOAL>Continuous ↿fun t => (γ t).extend
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Type u_4<VAR>TopologicalSpace ι<VAR>a b c : ι → X<VAR>γ₁ : (t : ι) → Path (a t) (b t)<VAR>h₁ : Continuous ↿γ₁<VAR>γ₂ : (t : ι) → Path (b t) (c t)<VAR>h₂ : Continuous ↿γ₂<GOAL>Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y z : X<VAR>f : Y → Path x y<VAR>g : Y → Path y z<GOAL>Continuous f → Continuous g → Continuous fun t => (f t).trans (g t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<GOAL>Continuous fun ρ => ρ.1.trans ρ.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a₁ a₂ : X<VAR>b₁ b₂ : Y<VAR>γ₁ : Path a₁ a₂<VAR>γ₂ : Path b₁ b₂<GOAL>⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a₁ a₂ a₃ : X<VAR>b₁ b₂ b₃ : Y<VAR>γ₁ : Path a₁ a₂<VAR>δ₁ : Path a₂ a₃<VAR>γ₂ : Path b₁ b₂<VAR>δ₂ : Path b₂ b₃<GOAL>(γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)
<VAR>ι : Type u_3<VAR>χ : ι → Type u_4<VAR>(i : ι) → TopologicalSpace (χ i)<VAR>as bs : (i : ι) → χ i<VAR>γ : (i : ι) → Path (as i) (bs i)<GOAL>⇑(Path.pi γ) = fun t i => (γ i) t
<VAR>ι : Type u_3<VAR>χ : ι → Type u_4<VAR>(i : ι) → TopologicalSpace (χ i)<VAR>as bs cs : (i : ι) → χ i<VAR>γ₀ : (i : ι) → Path (as i) (bs i)<VAR>γ₁ : (i : ι) → Path (bs i) (cs i)<GOAL>(Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Add X<VAR>ContinuousAdd X<VAR>a₁ b₁ a₂ b₂ : X<VAR>γ₁ : Path a₁ b₁<VAR>γ₂ : Path a₂ b₂<VAR>t : ↑I<GOAL>(γ₁.add γ₂) t = γ₁ t + γ₂ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Mul X<VAR>ContinuousMul X<VAR>a₁ b₁ a₂ b₂ : X<VAR>γ₁ : Path a₁ b₁<VAR>γ₂ : Path a₂ b₂<VAR>t : ↑I<GOAL>(γ₁.mul γ₂) t = γ₁ t * γ₂ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t₀ t₁ : ℝ<GOAL>Set.range ⇑(γ.truncate t₀ t₁) ⊆ Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>Continuous fun x => (γ.truncate x.1 x.2.1) x.2.2
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<GOAL>Continuous ↿(γ.truncate t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<GOAL>γ.truncate t t = (Path.refl (γ.extend t)).cast ⋯ ⋯
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.truncate 0 0 = (Path.refl a).cast ⋯ ⋯
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.truncate 1 1 = (Path.refl b).cast ⋯ ⋯
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>a b : X<VAR>γ : Path a b<GOAL>γ.truncate 0 1 = γ.cast ⋯ ⋯
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<VAR>f : ↑I → ↑I<VAR>hfcont : Continuous f<VAR>hf₀ : f 0 = 0<VAR>hf₁ : f 1 = 1<GOAL>⇑(γ.reparam f hfcont hf₀ hf₁) = ⇑γ ∘ f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>γ.reparam id ⋯ ⋯ ⋯ = γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<VAR>f : ↑I → ↑I<VAR>hfcont : Continuous f<VAR>hf₀ : f 0 = 0<VAR>hf₁ : f 1 = 1<GOAL>Set.range ⇑(γ.reparam f hfcont hf₀ hf₁) = Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>f : ↑I → ↑I<VAR>hfcont : Continuous f<VAR>hf₀ : f 0 = 0<VAR>hf₁ : f 1 = 1<GOAL>(Path.refl x).reparam f hfcont hf₀ hf₁ = Path.refl x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>Joined x x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : Joined x y<GOAL>Joined y x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>hxy : Joined x y<VAR>hyz : Joined y z<GOAL>Joined x z
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>x ∈ F ∧ y ∈ F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>x ∈ F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>y ∈ F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<VAR>t : ↑I<GOAL>h.somePath t ∈ F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>f : ℝ → X<VAR>hf : ContinuousOn f I<VAR>h₀ : f 0 = x<VAR>h₁ : f 1 = y<VAR>hF : f '' I ⊆ F<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>Joined x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>x_in : x ∈ F<VAR>y_in : y ∈ F<GOAL>JoinedIn F x y ↔ Joined ⟨x, x_in⟩ ⟨y, y_in⟩
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>JoinedIn Set.univ x y ↔ Joined x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>U V : Set X<VAR>h : JoinedIn U x y<VAR>hUV : U ⊆ V<GOAL>JoinedIn V x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>F : Set X<VAR>h : x ∈ F<GOAL>JoinedIn F x x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>JoinedIn F y x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>F : Set X<VAR>hxy : JoinedIn F x y<VAR>hyz : JoinedIn F y z<GOAL>JoinedIn F x z
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : x ⤳ y<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : Inseparable x y<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>x ∈ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>(pathComponent x).Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ∈ pathComponent y<GOAL>y ∈ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ∈ pathComponent y ↔ y ∈ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ∈ pathComponent y<GOAL>pathComponent x = pathComponent y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>pathComponent x ⊆ connectedComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>pathComponentIn x Set.univ = pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>hyz : Joined y z<VAR>hxy : y ∈ pathComponent x<GOAL>z ∈ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>F : Set X<GOAL>IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>F : Set X<VAR>h : IsPathConnected F<VAR>x : X<GOAL>x ∈ F → ∀ y ∈ F, JoinedIn F x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>F : Set X<GOAL>IsPathConnected F ↔ F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Set X<VAR>hF : IsPathConnected F<VAR>f : X → Y<VAR>hf : ContinuousOn f F<GOAL>IsPathConnected (f '' F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Set X<VAR>hF : IsPathConnected F<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsPathConnected (f '' F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsPathConnected F ↔ IsPathConnected (f '' F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>h : X ≃ₜ Y<GOAL>IsPathConnected (⇑h '' s) ↔ IsPathConnected s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>F : Set X<VAR>h : IsPathConnected F<VAR>x_in : x ∈ F<VAR>y_in : y ∈ F<GOAL>y ∈ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>F : Set X<VAR>h : IsPathConnected F<VAR>x_in : x ∈ F<GOAL>F ⊆ pathComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsPathConnected {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>U V : Set X<VAR>hU : IsPathConnected U<VAR>hV : IsPathConnected V<VAR>hUV : (U ∩ V).Nonempty<GOAL>IsPathConnected (U ∪ V)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>U W : Set X<VAR>hW : IsPathConnected W<VAR>hWU : W ⊆ U<GOAL>IsPathConnected (Subtype.val ⁻¹' W)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<GOAL>∃ γ, Set.range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>n : ℕ<VAR>s : Set X<VAR>h : IsPathConnected s<VAR>p : Fin (n + 1) → X<VAR>hp : ∀ (i : Fin (n + 1)), p i ∈ s<GOAL>∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : PathConnectedSpace X<GOAL>Nonempty X
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : PathConnectedSpace X<VAR>x y : X<GOAL>Joined x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>F : Set X<GOAL>IsPathConnected F ↔ PathConnectedSpace ↑F
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>PathConnectedSpace X ↔ IsPathConnected Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>PathConnectedSpace X<GOAL>IsPathConnected Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsPathConnected (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Function.Surjective f<VAR>hf' : Continuous f<GOAL>PathConnectedSpace Y
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>PathConnectedSpace X ↔ ∃ x, pathComponent x = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>F : Set X<VAR>hF : IsPathConnected F<GOAL>IsConnected F
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<GOAL>∃ γ, ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<GOAL>∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>self : LocPathConnectedSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>p : ι → Prop<VAR>s : X → ι → Set X<VAR>h : ∀ (x : X), (𝓝 x).HasBasis p (s x)<VAR>h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)<GOAL>LocPathConnectedSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocPathConnectedSpace X<GOAL>PathConnectedSpace X ↔ ConnectedSpace X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<VAR>hx : x ∈ U<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPathConnected s ∧ s ⊆ U) id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocPathConnectedSpace X<VAR>U : Set X<VAR>h : IsOpen U<GOAL>LocPathConnectedSpace ↑U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocPathConnectedSpace X<VAR>U : Set X<VAR>U_op : IsOpen U<GOAL>IsPathConnected U ↔ IsConnected U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>self : SmoothAdd I G<GOAL>Smooth (I.prod I) I fun p => p.1 + p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>self : SmoothMul I G<GOAL>Smooth (I.prod I) I fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<GOAL>Smooth (I.prod I) I fun p => p.1 + p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<GOAL>Smooth (I.prod I) I fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<GOAL>ContinuousMul G
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<GOAL>ContinuousAdd G
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I' I n f s x<VAR>hg : ContMDiffWithinAt I' I n g s x<GOAL>ContMDiffWithinAt I' I n (f + g) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I' I n f s x<VAR>hg : ContMDiffWithinAt I' I n g s x<GOAL>ContMDiffWithinAt I' I n (f * g) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffAt I' I n f x<VAR>hg : ContMDiffAt I' I n g x<GOAL>ContMDiffAt I' I n (f + g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffAt I' I n f x<VAR>hg : ContMDiffAt I' I n g x<GOAL>ContMDiffAt I' I n (f * g) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>s : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (f + g) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f g : M → G<VAR>s : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (f * g) s