ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>Filter.map (⇑h.symm) (𝓝 (h x)) = 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>𝓝 x = Filter.comap (⇑h) (𝓝 (h x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>y : Y<GOAL>Filter.comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>i : LocallyConnectedSpace Y<VAR>h : X ≃ₜ Y<GOAL>LocallyConnectedSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>LocallyCompactSpace X ↔ LocallyCompactSpace Y
<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>h : X ≃ₜ Y<VAR>f : Z → X<VAR>s : Set Z<GOAL>ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s
<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>h : X ≃ₜ Y<VAR>f : Z → X<GOAL>Continuous (⇑h ∘ f) ↔ Continuous 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>h : X ≃ₜ Y<VAR>f : Y → Z<GOAL>Continuous (f ∘ ⇑h) ↔ Continuous 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>h : X ≃ₜ Y<VAR>f : Z → X<VAR>z : Z<GOAL>ContinuousAt (⇑h ∘ f) z ↔ ContinuousAt f z
<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>h : X ≃ₜ Y<VAR>f : Y → Z<VAR>x : X<GOAL>ContinuousAt (f ∘ ⇑h) x ↔ ContinuousAt f (h 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>h : X ≃ₜ Y<VAR>f : Z → X<VAR>s : Set Z<VAR>z : Z<GOAL>ContinuousWithinAt f s z ↔ ContinuousWithinAt (⇑h ∘ f) s z
<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>h : X ≃ₜ Y<VAR>f : Z → X<GOAL>IsOpenMap (⇑h ∘ f) ↔ IsOpenMap 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>h : X ≃ₜ Y<VAR>f : Y → Z<GOAL>IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>h : X ≃ₜ Y<VAR>h_iff : ∀ (x : X), p x ↔ q (h x)<VAR>b : { b // q b }<GOAL>↑((h.subtype h_iff).symm b) = h.symm ↑b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>h : X ≃ₜ Y<VAR>h_iff : ∀ (x : X), p x ↔ q (h x)<VAR>a : { a // p a }<GOAL>↑((h.subtype h_iff) a) = h ↑a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>h : X ≃ₜ Y<VAR>h_iff : ∀ (x : X), p x ↔ q (h x)<GOAL>(h.subtype h_iff).toEquiv = h.subtypeEquiv h_iff
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y'<VAR>h₁ : X ≃ₜ X'<VAR>h₂ : Y ≃ₜ Y'<GOAL>(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y'<VAR>h₁ : X ≃ₜ X'<VAR>h₂ : Y ≃ₜ Y'<GOAL>⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>(Homeomorph.prodComm X Y).symm = Homeomorph.prodComm Y X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>⇑(Homeomorph.prodComm X Y) = Prod.swap
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.prodPUnit X) = fun p => p.1
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.punitProd X) = Prod.snd
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Unique X<VAR>Unique Y<GOAL>∀ (a : X), (Homeomorph.homeomorphOfUnique X Y) a = default
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Unique X<VAR>Unique Y<GOAL>∀ (a : Y), (Homeomorph.homeomorphOfUnique X Y).symm a = default
<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>Y : ι' → Type u_8<VAR>(j : ι') → TopologicalSpace (Y j)<VAR>e : ι ≃ ι'<GOAL>(Homeomorph.piCongrLeft e).toEquiv = Equiv.piCongrLeft Y e
<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>Y : ι' → Type u_8<VAR>(j : ι') → TopologicalSpace (Y j)<VAR>e : ι ≃ ι'<GOAL>∀ (a : (b : ι) → Y (e.symm.symm b)) (a_1 : ι'), (Homeomorph.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' Y e.symm).symm a a_1
<VAR>ι : Type u_6<VAR>Y₁ : ι → Type u_7<VAR>Y₂ : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (Y₁ i)<VAR>(i : ι) → TopologicalSpace (Y₂ i)<VAR>F : (i : ι) → Y₁ i ≃ₜ Y₂ i<VAR>H : (a : ι) → Y₁ a<VAR>a : ι<GOAL>(Homeomorph.piCongrRight F) H a = (F a) (H a)
<VAR>ι : Type u_6<VAR>Y₁ : ι → Type u_7<VAR>Y₂ : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (Y₁ i)<VAR>(i : ι) → TopologicalSpace (Y₂ i)<VAR>F : (i : ι) → Y₁ i ≃ₜ Y₂ i<GOAL>(Homeomorph.piCongrRight F).toEquiv = Equiv.piCongrRight fun i => (F i).toEquiv
<VAR>ι : Type u_6<VAR>Y₁ : ι → Type u_7<VAR>Y₂ : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (Y₁ i)<VAR>(i : ι) → TopologicalSpace (Y₂ i)<VAR>F : (i : ι) → Y₁ i ≃ₜ Y₂ i<GOAL>(Homeomorph.piCongrRight F).symm = Homeomorph.piCongrRight fun i => (F i).symm
<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>Y₁ : ι₁ → Type u_8<VAR>Y₂ : ι₂ → Type u_9<VAR>(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)<VAR>(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)<VAR>e : ι₁ ≃ ι₂<VAR>F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)<GOAL>∀ (a : (i : ι₁) → Y₁ i) (i₂ : ι₂), (Homeomorph.piCongr e F) a i₂ = ⋯ ▸ (Equiv.piCongrRight fun i => (F i).toEquiv) a (e.symm i₂)
<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>Y₁ : ι₁ → Type u_8<VAR>Y₂ : ι₂ → Type u_9<VAR>(i₁ : ι₁) → TopologicalSpace (Y₁ i₁)<VAR>(i₂ : ι₂) → TopologicalSpace (Y₂ i₂)<VAR>e : ι₁ ≃ ι₂<VAR>F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)<GOAL>(Homeomorph.piCongr e F).toEquiv = (Equiv.piCongrRight fun i => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)
<VAR>ι : Type u_6<VAR>X : Type u_7<VAR>Unique ι<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.funUnique ι X).symm = uniqueElim
<VAR>ι : Type u_6<VAR>X : Type u_7<VAR>Unique ι<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.funUnique ι X) = fun f => f default
<VAR>X : Fin 2 → Type u<VAR>(i : Fin 2) → TopologicalSpace (X i)<GOAL>⇑(Homeomorph.piFinTwo X) = fun f => (f 0, f 1)
<VAR>X : Fin 2 → Type u<VAR>(i : Fin 2) → TopologicalSpace (X i)<GOAL>⇑(Homeomorph.piFinTwo X).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>⇑Homeomorph.finTwoArrow = fun f => (f 0, f 1)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>⇑Homeomorph.finTwoArrow.symm = fun x => ![x.1, x.2]
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>x : ↑s<GOAL>↑((e.image s) x) = e ↑x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>y : ↑(⇑e.toEquiv '' s)<GOAL>↑((e.image s).symm y) = e.symm ↑y
<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>a : X<GOAL>↑((Homeomorph.Set.univ X).symm a) = a
<VAR>X : Type u_6<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.Set.univ X) = Subtype.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : { a // s a } × { b // t b }<GOAL>↑((Homeomorph.Set.prod s t).symm x) = (↑x.1, ↑x.2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : { c // s c.1 ∧ t c.2 }<GOAL>(Homeomorph.Set.prod s t) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)
<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>Y : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>DecidablePred p<VAR>f : (i : ι) → Y i<GOAL>(Homeomorph.piEquivPiSubtypeProd p Y) f = (fun x => f ↑x, fun x => f ↑x)
<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>Y : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>DecidablePred p<VAR>f : ((i : { x // p x }) → Y ↑i) × ((i : { x // ¬p x }) → Y ↑i)<VAR>x : ι<GOAL>(Homeomorph.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>i : ι<VAR>Y : ι → Type u_7<VAR>(j : ι) → TopologicalSpace (Y j)<VAR>f : Y i × ((j : { j // j ≠ i }) → Y ↑j)<VAR>j : ι<GOAL>(Homeomorph.piSplitAt i Y).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩
<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>i : ι<VAR>Y : ι → Type u_7<VAR>(j : ι) → TopologicalSpace (Y j)<VAR>f : (j : ι) → Y j<GOAL>(Homeomorph.piSplitAt i Y) f = (f i, fun j => f ↑j)
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → (fun a => Y) j<GOAL>(Homeomorph.funSplitAt Y i) f = (f i, fun j => f ↑j)
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (fun a => Y) i × ((j : { j // j ≠ i }) → (fun a => Y) ↑j)<VAR>j : ι<GOAL>(Homeomorph.funSplitAt Y i).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<GOAL>(e.toHomeomorph he).toEquiv = e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<GOAL>⇑(e.toHomeomorph he) = ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<VAR>x : X<GOAL>(e.toHomeomorph he) x = e x
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ Y<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<GOAL>(e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : X ≃ Y<VAR>f : Y ≃ Z<VAR>he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s<VAR>hf : ∀ (s : Set Z), IsOpen (⇑f ⁻¹' s) ↔ IsOpen s<GOAL>(e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X ≃ Y<VAR>hf : Inducing ⇑f<GOAL>(f.toHomeomorphOfInducing hf).toEquiv = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑f.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<GOAL>hf.homeoOfEquivCompactToT2.toEquiv = f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SigmaCompactSpace M<VAR>T2Space M<GOAL>TopologicalSpace.MetrizableSpace M
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>W : TopologicalSpace.Clopens (X × Y)<VAR>a : X × Y<VAR>h : a ∈ W<GOAL>∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>CompactSpace X<VAR>W : TopologicalSpace.Clopens (X × Y)<GOAL>∃ I, W = I.sup fun i => i.1 ×ˢ i.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>CompactSpace X<GOAL>Function.Surjective fun I => I.sup fun i => i.1 ×ˢ i.2
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>TotallyDisconnectedSpace X<GOAL>Countable (TopologicalSpace.Clopens X) ↔ SecondCountableTopology X
<VAR>A : Type u_7<VAR>B : Type u_8<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : ContinuousAddMonoidHom A B<GOAL>Continuous (↑self.toAddMonoidHom).toFun
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : ContinuousMonoidHom A B<GOAL>Continuous (↑self.toMonoidHom).toFun
<VAR>F : Type u_1<VAR>A : outParam (Type u_7)<VAR>B : outParam (Type u_8)<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>FunLike F A B<VAR>self : ContinuousAddMonoidHomClass F A B<VAR>f : F<GOAL>Continuous ⇑f
<VAR>F : Type u_1<VAR>A : outParam (Type u_7)<VAR>B : outParam (Type u_8)<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>FunLike F A B<VAR>self : ContinuousMonoidHomClass F A B<VAR>f : F<GOAL>Continuous ⇑f
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>f g : ContinuousAddMonoidHom A B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>f g : ContinuousMonoidHom A B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Function.Injective ContinuousAddMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Function.Injective ContinuousMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>g : ContinuousAddMonoidHom B C<VAR>f : ContinuousAddMonoidHom A B<GOAL>∀ (a : A), (g.comp f) a = g.toAddMonoidHom (f.toAddMonoidHom a)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>g : ContinuousMonoidHom B C<VAR>f : ContinuousMonoidHom A B<GOAL>∀ (a : A), (g.comp f) a = g.toMonoidHom (f.toMonoidHom a)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousMonoidHom A B<VAR>g : ContinuousMonoidHom A C<VAR>i : A<GOAL>(f.prod g) i = (f.toMonoidHom i, g.toMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousAddMonoidHom A B<VAR>g : ContinuousAddMonoidHom A C<VAR>i : A<GOAL>(f.sum g) i = (f.toAddMonoidHom i, g.toAddMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>AddMonoid D<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>TopologicalSpace D<VAR>f : ContinuousAddMonoidHom A C<VAR>g : ContinuousAddMonoidHom B D<VAR>i : A × B<GOAL>(f.sum_map g) i = (f.toAddMonoidHom i.1, g.toAddMonoidHom i.2)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>Monoid D<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>TopologicalSpace D<VAR>f : ContinuousMonoidHom A C<VAR>g : ContinuousMonoidHom B D<VAR>i : A × B<GOAL>(f.prod_map g) i = (f.toMonoidHom i.1, g.toMonoidHom i.2)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>∀ (x : A), (ContinuousAddMonoidHom.zero A B) x = 0
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>∀ (x : A), (ContinuousMonoidHom.one A B) x = 1
<VAR>A : Type u_2<VAR>Monoid A<VAR>TopologicalSpace A<VAR>x : A<GOAL>(ContinuousMonoidHom.id A) x = x
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>TopologicalSpace A<VAR>x : A<GOAL>(ContinuousAddMonoidHom.id A) x = x
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : A × B<GOAL>(ContinuousAddMonoidHom.fst A B) self = self.1
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : A × B<GOAL>(ContinuousMonoidHom.fst A B) self = self.1
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : A × B<GOAL>(ContinuousAddMonoidHom.snd A B) self = self.2
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>self : A × B<GOAL>(ContinuousMonoidHom.snd A B) self = self.2
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : A<GOAL>(ContinuousMonoidHom.inl A B) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.one A B).toMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : A<GOAL>(ContinuousAddMonoidHom.inl A B) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.zero A B).toAddMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : B<GOAL>(ContinuousMonoidHom.inr A B) i = ((ContinuousMonoidHom.one B A).toMonoidHom i, (ContinuousMonoidHom.id B).toMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : B<GOAL>(ContinuousAddMonoidHom.inr A B) i = ((ContinuousAddMonoidHom.zero B A).toAddMonoidHom i, (ContinuousAddMonoidHom.id B).toAddMonoidHom i)
<VAR>A : Type u_2<VAR>Monoid A<VAR>TopologicalSpace A<VAR>i : A<GOAL>(ContinuousMonoidHom.diag A) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.id A).toMonoidHom i)
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>TopologicalSpace A<VAR>i : A<GOAL>(ContinuousAddMonoidHom.diag A) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.id A).toAddMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : A × B<GOAL>(ContinuousAddMonoidHom.swap A B) i = ((ContinuousAddMonoidHom.snd A B).toAddMonoidHom i, (ContinuousAddMonoidHom.fst A B).toAddMonoidHom i)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>i : A × B<GOAL>(ContinuousMonoidHom.swap A B) i = ((ContinuousMonoidHom.snd A B).toMonoidHom i, (ContinuousMonoidHom.fst A B).toMonoidHom i)
<VAR>E : Type u_6<VAR>CommGroup E<VAR>TopologicalSpace E<VAR>TopologicalGroup E<GOAL>∀ (a : E × E), (ContinuousMonoidHom.mul E) a = a.1 * a.2
<VAR>E : Type u_6<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<GOAL>∀ (a : E × E), (ContinuousAddMonoidHom.add E) a = a.1 + a.2
<VAR>E : Type u_6<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<GOAL>∀ (a : E), (ContinuousAddMonoidHom.neg E) a = -a
<VAR>E : Type u_6<VAR>CommGroup E<VAR>TopologicalSpace E<VAR>TopologicalGroup E<GOAL>∀ (a : E), (ContinuousMonoidHom.inv E) a = a⁻¹
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>E : Type u_6<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddCommGroup E<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>f : ContinuousAddMonoidHom A E<VAR>g : ContinuousAddMonoidHom B E<GOAL>∀ (a : A × B), (f.coprod g) a = (ContinuousAddMonoidHom.add E).toAddMonoidHom ((f.sum_map g).toAddMonoidHom a)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>E : Type u_6<VAR>Monoid A<VAR>Monoid B<VAR>CommGroup E<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace E<VAR>TopologicalGroup E<VAR>f : ContinuousMonoidHom A E<VAR>g : ContinuousMonoidHom B E<GOAL>∀ (a : A × B), (f.coprod g) a = (ContinuousMonoidHom.mul E).toMonoidHom ((f.prod_map g).toMonoidHom a)
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Inducing ContinuousMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Inducing ContinuousAddMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Embedding ContinuousAddMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Embedding ContinuousMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Set.range ContinuousAddMonoidHom.toContinuousMap = {f | f 0 = 0 ∧ ∀ (x y : A), f (x + y) = f x + f y}
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<GOAL>Set.range ContinuousMonoidHom.toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>ContinuousAdd B<VAR>T2Space B<GOAL>ClosedEmbedding ContinuousAddMonoidHom.toContinuousMap
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid A<VAR>Monoid B<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>ContinuousMul B<VAR>T2Space B<GOAL>ClosedEmbedding ContinuousMonoidHom.toContinuousMap
<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>A : Type u_7<VAR>TopologicalSpace A<VAR>f : A → ContinuousAddMonoidHom B C<VAR>h : Continuous (Function.uncurry fun x y => (f x) y)<GOAL>Continuous f
<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>A : Type u_7<VAR>TopologicalSpace A<VAR>f : A → ContinuousMonoidHom B C<VAR>h : Continuous (Function.uncurry fun x y => (f x) y)<GOAL>Continuous f
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>LocallyCompactSpace B<GOAL>Continuous fun f => f.2.comp f.1
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>LocallyCompactSpace B<GOAL>Continuous fun f => f.2.comp f.1
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousMonoidHom A B<GOAL>Continuous fun g => g.comp f
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousAddMonoidHom A B<GOAL>Continuous fun g => g.comp f
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>AddMonoid A<VAR>AddMonoid B<VAR>AddMonoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousAddMonoidHom B C<GOAL>Continuous fun g => f.comp g
<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid A<VAR>Monoid B<VAR>Monoid C<VAR>TopologicalSpace A<VAR>TopologicalSpace B<VAR>TopologicalSpace C<VAR>f : ContinuousMonoidHom B C<GOAL>Continuous fun g => f.comp g
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>Group X<VAR>TopologicalGroup X<VAR>UniformSpace Y<VAR>CommGroup Y<VAR>UniformGroup Y<VAR>T0Space Y<VAR>CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>h : EquicontinuousAt (fun f => ⇑↑f) 1<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>AddGroup X<VAR>TopologicalAddGroup X<VAR>UniformSpace Y<VAR>AddCommGroup Y<VAR>UniformAddGroup Y<VAR>T0Space Y<VAR>CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 0<VAR>h : EquicontinuousAt (fun f => ⇑↑f) 0<GOAL>LocallyCompactSpace (ContinuousAddMonoidHom X Y)
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>Group X<VAR>TopologicalGroup X<VAR>UniformSpace Y<VAR>CommGroup Y<VAR>UniformGroup Y<VAR>T0Space Y<VAR>CompactSpace Y<VAR>LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)