ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>F : Filter X<GOAL>(Filter.map f F).lift' closure = Filter.map f (F.lift' closure)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>F : Filter X<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>y : Y<GOAL>MapClusterPt y F f ↔ (F.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<VAR>x : X<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<VAR>s : Set X<GOAL>IsOpen s ↔ IsOpen (f '' s)
<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>g : Y → Z<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : ι → Y<VAR>l : Filter ι<VAR>y : Y<VAR>hg : OpenEmbedding g<GOAL>Filter.Tendsto f l (𝓝 y) ↔ Filter.Tendsto (g ∘ f) l (𝓝 (g y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<VAR>l : Filter Z<VAR>x : X<GOAL>Filter.Tendsto (g ∘ f) (𝓝 x) l ↔ Filter.Tendsto g (𝓝 (f x)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hf : OpenEmbedding f<VAR>x : X<GOAL>ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : OpenEmbedding f<VAR>s : Set Y<VAR>hs : s ⊆ Set.range f<GOAL>IsOpen s ↔ IsOpen (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h₁ : Embedding f<VAR>h₂ : IsOpenMap f<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : Embedding f<VAR>hsurj : Function.Surjective f<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>OpenEmbedding f ↔ Embedding f ∧ IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h₁ : Continuous f<VAR>h₂ : Function.Injective f<VAR>h₃ : IsOpenMap f<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>OpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>OpenEmbedding id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : OpenEmbedding g<VAR>hf : OpenEmbedding f<GOAL>OpenEmbedding (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : OpenEmbedding g<GOAL>IsOpenMap f ↔ IsOpenMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>hg : OpenEmbedding g<GOAL>OpenEmbedding (g ∘ f) ↔ OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>hg : OpenEmbedding g<VAR>h : OpenEmbedding (g ∘ f)<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>IsEmpty X<VAR>f : X → Y<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_4<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>g : ι → X<VAR>l : Filter ι<VAR>x : X<VAR>hf : ClosedEmbedding f<GOAL>Filter.Tendsto g l (𝓝 x) ↔ Filter.Tendsto (f ∘ g) l (𝓝 (f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ClosedEmbedding f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ClosedEmbedding f<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ClosedEmbedding f<VAR>s : Set X<GOAL>IsClosed s ↔ IsClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ClosedEmbedding f<VAR>s : Set Y<VAR>hs : s ⊆ Set.range f<GOAL>IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h₁ : Embedding f<VAR>h₂ : IsClosedMap f<GOAL>ClosedEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h₁ : Continuous f<VAR>h₂ : Function.Injective f<VAR>h₃ : IsClosedMap f<GOAL>ClosedEmbedding f
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>ClosedEmbedding id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : ClosedEmbedding g<VAR>hf : ClosedEmbedding f<GOAL>ClosedEmbedding (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>f : X → Y<VAR>g : Y → Z<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>hg : ClosedEmbedding g<GOAL>ClosedEmbedding (g ∘ f) ↔ ClosedEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>f : X → Y<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>hf : ClosedEmbedding f<VAR>s : Set X<GOAL>closure (f '' s) = f '' closure s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>self : IsProperMap f<VAR>ℱ : Filter X<VAR>y : Y<GOAL>MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : IsProperMap f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : IsProperMap f<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : IsProperMap f<VAR>𝒰 : Ultrafilter X<VAR>y : Y<VAR>hy : Filter.Tendsto f (↑𝒰) (𝓝 y)<GOAL>∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<GOAL>IsProperMap (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>f_surj : Function.Surjective f<GOAL>IsProperMap g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>g_inj : Function.Injective g<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace W<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsProperMap f<VAR>hg : IsProperMap g<GOAL>IsProperMap (Prod.map f g)
<VAR>ι : Type u_5<VAR>X : ι → Type u_6<VAR>Y : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (X i)<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>f : (i : ι) → X i → Y i<VAR>h : ∀ (i : ι), IsProperMap (f i)<GOAL>IsProperMap fun x i => f i (x i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>f_cont : Continuous f<VAR>f_inj : Function.Injective f<GOAL>IsProperMap f ↔ IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>f_cont : Continuous f<VAR>f_inj : Function.Injective f<VAR>f_closed : IsClosedMap f<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>IsProperMap ⇑e
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsProperMap id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>U : Set X<VAR>hU : IsClosed U<GOAL>IsProperMap Subtype.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>U : Set X<VAR>hf : IsProperMap f<VAR>hU : IsClosed U<GOAL>IsProperMap fun x => f ↑x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsProperMap f<GOAL>IsClosed (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T1Space Y<GOAL>IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Filter.Tendsto f (Filter.cocompact X) Filter.cofinite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>hf : Continuous f<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>WeaklyLocallyCompactSpace X<VAR>s : Set X<GOAL>IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>WeaklyLocallyCompactSpace Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>SequentialSpace X<VAR>s : Set X<GOAL>IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>SequentialSpace Y<GOAL>IsProperMap f ↔ Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>WeaklyLocallyCompactSpace Y<GOAL>IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>T2Space Y<VAR>SequentialSpace Y<GOAL>IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>Z : Type u_6<VAR>TopologicalSpace Z<VAR>h : IsProperMap f<GOAL>IsClosedMap (Prod.map f id)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>A : Set X<VAR>f : X → Y<VAR>x : X<VAR>h : ∃ y, Filter.Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>Filter.Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>A : Set X<VAR>f : X → Y<VAR>x : X<VAR>y : Y<VAR>hx : x ∈ closure A<VAR>hf : Filter.Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>extendFrom A f x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>A : Set X<VAR>hf : ContinuousOn f A<VAR>x : X<GOAL>x ∈ A → extendFrom A f x = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>RegularSpace Y<VAR>f : X → Y<VAR>A B : Set X<VAR>hB : B ⊆ closure A<VAR>hf : ∀ x ∈ B, ∃ y, Filter.Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>ContinuousOn (extendFrom A f) B
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>RegularSpace Y<VAR>f : X → Y<VAR>A : Set X<VAR>hA : Dense A<VAR>hf : ∀ (x : X), ∃ y, Filter.Tendsto f (𝓝[A] x) (𝓝 y)<GOAL>Continuous (extendFrom A f)
<VAR>I : Type u_1<VAR>A : Type u_2<VAR>X : I → Type u_3<VAR>(i : I) → TopologicalSpace (X i)<VAR>TopologicalSpace A<VAR>f g : (i : I) → C(A, X i)<VAR>S : Set A<VAR>homotopies : (i : I) → (f i).HomotopyRel (g i) S<VAR>a : ↑unitInterval × A<VAR>i : I<GOAL>(ContinuousMap.HomotopyRel.pi homotopies) a i = (homotopies i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>f₀ f₁ : C(A, α)<VAR>g₀ g₁ : C(A, β)<VAR>F : f₀.Homotopy f₁<VAR>G : g₀.Homotopy g₁<VAR>t : ↑unitInterval × A<GOAL>(F.prod G) t = (F t, G t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>f₀ f₁ : C(A, α)<VAR>g₀ g₁ : C(A, β)<VAR>S : Set A<VAR>F : f₀.HomotopyRel f₁ S<VAR>G : g₀.HomotopyRel g₁ S<VAR>t : ↑unitInterval × A<GOAL>(F.prod G) t = (F t, G t)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>as bs : (i : ι) → X i<VAR>γ : (i : ι) → Path (as i) (bs i)<GOAL>(Path.Homotopic.pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>γ₀ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)<VAR>γ₁ : (i : ι) → Path.Homotopic.Quotient (bs i) (cs i)<GOAL>(Path.Homotopic.pi γ₀).comp (Path.Homotopic.pi γ₁) = Path.Homotopic.pi fun i => (γ₀ i).comp (γ₁ i)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>as bs : (i : ι) → X i<VAR>i : ι<VAR>paths : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)<GOAL>Path.Homotopic.proj i (Path.Homotopic.pi paths) = paths i
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>as bs : (i : ι) → X i<VAR>p : Path.Homotopic.Quotient as bs<GOAL>(Path.Homotopic.pi fun i => Path.Homotopic.proj i p) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>p₁ : Path a₁ a₂<VAR>p₂ : Path b₁ b₂<GOAL>Path.Homotopic.prod ⟦p₁⟧ ⟦p₂⟧ = ⟦p₁.prod p₂⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>q₁ : Path.Homotopic.Quotient a₁ a₂<VAR>q₂ : Path.Homotopic.Quotient b₁ b₂<VAR>r₁ : Path.Homotopic.Quotient a₂ a₃<VAR>r₂ : Path.Homotopic.Quotient b₂ b₃<GOAL>(Path.Homotopic.prod q₁ q₂).comp (Path.Homotopic.prod r₁ r₂) = Path.Homotopic.prod (q₁.comp r₁) (q₂.comp r₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>q₁ : Path.Homotopic.Quotient a₁ a₂<VAR>q₂ : Path.Homotopic.Quotient b₁ b₂<GOAL>Path.Homotopic.projLeft (Path.Homotopic.prod q₁ q₂) = q₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>q₁ : Path.Homotopic.Quotient a₁ a₂<VAR>q₂ : Path.Homotopic.Quotient b₁ b₂<GOAL>Path.Homotopic.projRight (Path.Homotopic.prod q₁ q₂) = q₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)<GOAL>Path.Homotopic.prod (Path.Homotopic.projLeft p) (Path.Homotopic.projRight p) = p
<VAR>x y : ℤ<GOAL>dist x y = |↑x - ↑y|
<GOAL>Pairwise fun m n => 1 ≤ dist m n
<VAR>x : ℤ<VAR>r : ℝ<GOAL>Int.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
<VAR>x : ℤ<VAR>r : ℝ<GOAL>Int.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
<VAR>x : ℤ<VAR>r : ℝ<GOAL>Metric.ball x r = Set.Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
<VAR>x : ℤ<VAR>r : ℝ<GOAL>Metric.closedBall x r = Set.Icc ⌈↑x - r⌉ ⌊↑x + r⌋
<GOAL>Bornology.cobounded ℤ = Filter.atBot ⊔ Filter.atTop
<GOAL>Filter.cofinite = Filter.atBot ⊔ Filter.atTop
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : HSpace X<GOAL>HSpace.hmul (HSpace.e, HSpace.e) = HSpace.e
<VAR>G : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>1 = HSpace.e
<VAR>θ : ↑I<GOAL>unitInterval.qRight (0, θ) = 0
<VAR>θ : ↑I<GOAL>unitInterval.qRight (1, θ) = 1
<VAR>t : ↑I<GOAL>↑(unitInterval.qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
<VAR>t : ↑I<GOAL>unitInterval.qRight (t, 1) = t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Continuous fun p => Path.delayReflRight p.1 p.2
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Path.delayReflRight 0 γ = γ.trans (Path.refl y)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Path.delayReflRight 1 γ = γ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Continuous fun p => Path.delayReflLeft p.1 p.2
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Path.delayReflLeft 0 γ = (Path.refl x).trans γ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>Path.delayReflLeft 1 γ = γ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : IsIrreducible s<GOAL>s.Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : IsIrreducible s<GOAL>IsPreirreducible s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsPreirreducible ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<GOAL>IsPreirreducible s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsPreirreducible {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsIrreducible {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsPreirreducible (closure s) ↔ IsPreirreducible s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsIrreducible (closure s) ↔ IsIrreducible s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>H : IsPreirreducible s<GOAL>∃ t, IsPreirreducible t ∧ s ⊆ t ∧ ∀ (u : Set X), IsPreirreducible u → t ⊆ u → u = t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>H : s ∈ irreducibleComponents X<GOAL>IsClosed s
<VAR>X : Type u_3<VAR>TopologicalSpace X<GOAL>irreducibleComponents X = maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsPreirreducible (irreducibleComponent x) ∧ {x} ⊆ irreducibleComponent x ∧ ∀ (u : Set X), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>x ∈ irreducibleComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsIrreducible (irreducibleComponent x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>x : X<GOAL>IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>irreducibleComponent x ∈ irreducibleComponents X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsClosed (irreducibleComponent x)
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>self : PreirreducibleSpace X<GOAL>IsPreirreducible Set.univ
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>self : IrreducibleSpace X<GOAL>Nonempty X
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>IrreducibleSpace X<GOAL>IsIrreducible Set.univ
<VAR>X : Type u_3<VAR>TopologicalSpace X<GOAL>IrreducibleSpace X ↔ IsIrreducible ⊤
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>PreirreducibleSpace X<GOAL>IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>PreirreducibleSpace X<VAR>ho : IsOpen s<VAR>hne : s.Nonempty<GOAL>Dense s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<GOAL>IsPreirreducible (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>H : IsIrreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<GOAL>IsIrreducible (f '' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : IsPreirreducible s<GOAL>PreirreducibleSpace ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : IsIrreducible s<GOAL>IrreducibleSpace ↑s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsIrreducible s ↔ ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S U : Set X<VAR>hS : IsPreirreducible S<VAR>hU : IsOpen U<VAR>h : (S ∩ U).Nonempty<GOAL>S ⊆ closure (S ∩ U)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t S U : Set X<VAR>ht : IsPreirreducible t<VAR>hU : U.Nonempty<VAR>hU' : IsOpen U<VAR>h₁ : U ⊆ S<VAR>h₂ : S ⊆ t<GOAL>IsIrreducible S
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t U : Set X<VAR>ht : IsPreirreducible t<VAR>hU : IsOpen U<VAR>hU' : U ⊆ t<GOAL>IsPreirreducible U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t : Set X<VAR>ht : IsPreirreducible t<GOAL>IsPreirreducible (interior t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>t : Set X<VAR>ht : IsPreirreducible t<VAR>f : Y → X<VAR>hf : OpenEmbedding f<GOAL>IsPreirreducible (f ⁻¹' t)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c : R<VAR>x : R<VAR>e : ℕ<VAR>pq_pf : a + b = c<GOAL>x ^ e * a + x ^ e * b = x ^ e * c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b : R<VAR>x : R<VAR>e : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat (a + b) 0 → Mathlib.Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b : R<GOAL>0 + b = b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a + 0 = a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₁ a₂ b₁ b₂ c₁ c₂ : R<GOAL>a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₁ a₂ b₁ b₂ c : R<VAR>h : Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0<VAR>h₄ : a₂ + b₂ = c<GOAL>a₁ + a₂ + (b₁ + b₂) = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₂ b c : R<VAR>a₁ : R<GOAL>a₂ + b = c → a₁ + a₂ + b = a₁ + c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b₂ c : R<VAR>b₁ : R<GOAL>a + b₂ = c → a + (b₁ + b₂) = b₁ + c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>Nat.rawCast 1 * a = a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a * Nat.rawCast 1 = a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₃ b c : R<VAR>a₁ : R<VAR>a₂ : ℕ<GOAL>a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b₃ c : R<VAR>b₁ : R<VAR>b₂ : ℕ<GOAL>a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₂ b₂ c : R<VAR>ea eb e : ℕ<VAR>x : R<GOAL>ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a * 0 = 0