ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>n : ℕ<VAR>f : M [⋀^Fin (n + 1)]→L[R] N<VAR>m : Fin n → M<VAR>c : R<VAR>x : M<GOAL>f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m m' : ι → M<VAR>t : Finset ι<GOAL>f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m m' : ι → M<GOAL>f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>α : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>g' : (i : ι) → α i → M<VAR>A : (i : ι) → Finset (α i)<GOAL>(f fun i => ∑ j ∈ A i, g' i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g' i (r i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>α : ι → Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>g' : (i : ι) → α i → M<VAR>(i : ι) → Fintype (α i)<GOAL>(f fun i => ∑ j : α i, g' i j) = ∑ r : (i : ι) → α i, f fun i => g' i (r i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>A : Type u_7<VAR>Semiring A<VAR>SMul R A<VAR>Module A M<VAR>Module A N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>f : M [⋀^ι]→L[A] N<GOAL>⇑(ContinuousAlternatingMap.restrictScalars R f) = ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<VAR>x y : M<GOAL>f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>TopologicalAddGroup N<GOAL>⇑(-f) = -⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>TopologicalAddGroup N<VAR>m : ι → M<GOAL>(-f) m = -f m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<VAR>TopologicalAddGroup N<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<VAR>TopologicalAddGroup N<VAR>m : ι → M<GOAL>(f - g) m = f m - g m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>c : ι → R<VAR>m : ι → M<VAR>s : Finset ι<GOAL>f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>Fintype ι<VAR>c : ι → R<VAR>m : ι → M<GOAL>(f fun i => c i • m i) = (∏ i : ι, c i) • f m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>Semiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>Module A M<VAR>Module A N<VAR>Module R N<VAR>ContinuousConstSMul R N<VAR>SMulCommClass A R N<VAR>self : M [⋀^ι]→L[A] N<GOAL>ContinuousAlternatingMap.toContinuousMultilinearMapLinear self = self.toContinuousMultilinearMap
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>Semiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>Module A M<VAR>Module A N<VAR>Module R N<VAR>ContinuousConstSMul R N<VAR>SMulCommClass A R N<GOAL>⇑ContinuousAlternatingMap.toAlternatingMapLinear = ContinuousAlternatingMap.toAlternatingMap
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>Semiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>Module A M<VAR>ι' : Type u_6<VAR>M' : ι' → Type u_7<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>∀ (i : ι'), ContinuousAdd (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>(i : ι') → Module A (M' i)<VAR>∀ (i : ι'), SMulCommClass A R (M' i)<VAR>∀ (i : ι'), ContinuousConstSMul R (M' i)<GOAL>∀ (a : (i : ι') → M [⋀^ι]→L[A] M' i), ContinuousAlternatingMap.piLinearEquiv a = ContinuousAlternatingMap.pi a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>Semiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>Module A M<VAR>ι' : Type u_6<VAR>M' : ι' → Type u_7<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>∀ (i : ι'), ContinuousAdd (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>(i : ι') → Module A (M' i)<VAR>∀ (i : ι'), SMulCommClass A R (M' i)<VAR>∀ (i : ι'), ContinuousConstSMul R (M' i)<GOAL>∀ (a : M [⋀^ι]→L[A] ((i : ι') → M' i)) (i : ι'), ContinuousAlternatingMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap a
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousSMul R N<VAR>f : M [⋀^ι]→L[R] R<VAR>z : N<GOAL>∀ (a : (i : ι) → (fun x => M) i), (f.smulRight z) a = f a • z
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>TopologicalSpace N<VAR>ContinuousSMul R N<VAR>f : M [⋀^ι]→L[R] R<VAR>z : N<GOAL>(f.smulRight z).toContinuousMultilinearMap = f.smulRight z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>TopologicalSpace M'<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>ContinuousConstSMul R N<VAR>f : M →L[R] M'<VAR>g : M' [⋀^ι]→L[R] N<GOAL>(ContinuousAlternatingMap.compContinuousLinearMapₗ f) g = g.compContinuousLinearMap f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : ContinuousMultilinearMap R (fun x => M) N<GOAL>(ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : ContinuousMultilinearMap R (fun x => M) N<VAR>v : ι → M<GOAL>(ContinuousMultilinearMap.alternatization f) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f (v ∘ ⇑σ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommGroup N<VAR>Module R N<VAR>TopologicalSpace N<VAR>TopologicalAddGroup N<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : ContinuousMultilinearMap R (fun x => M) N<GOAL>(ContinuousMultilinearMap.alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>IsTotallyDisconnected ∅
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsTotallyDisconnected {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>self : TotallyDisconnectedSpace α<GOAL>IsTotallyDisconnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>TotallyDisconnectedSpace α ↔ IsTotallyDisconnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>TotallyDisconnectedSpace α<VAR>s : Set α<VAR>h : IsPreconnected s<GOAL>s.Subsingleton
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<GOAL>IsTotallyDisconnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>TotallyDisconnectedSpace α<VAR>x : α<GOAL>connectedComponent x = {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>a : α<GOAL>f '' connectedComponent a = {f a}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>TotallyDisconnectedSpace α<VAR>s : Set α<GOAL>IsTotallyDisconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>s : Set α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>hf' : Function.Injective f<VAR>h : IsTotallyDisconnected (f '' s)<GOAL>IsTotallyDisconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Embedding f<VAR>s : Set α<VAR>h : IsTotallyDisconnected (f '' s)<GOAL>IsTotallyDisconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Embedding f<VAR>s : Set α<GOAL>IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Embedding f<GOAL>IsTotallyDisconnected (Set.range f) ↔ TotallyDisconnectedSpace α
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>IsTotallySeparated ∅
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsTotallySeparated {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : IsTotallySeparated s<GOAL>IsTotallyDisconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>self : TotallySeparatedSpace α<GOAL>IsTotallySeparated Set.univ
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>TotallySeparatedSpace α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>a b : α<VAR>hab : connectedComponent a = connectedComponent b<GOAL>f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>Continuous h.connectedComponentsLift
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>x : α<GOAL>h.connectedComponentsLift (ConnectedComponents.mk x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>h.connectedComponentsLift ∘ ConnectedComponents.mk = f
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Sort u_3<VAR>g₁ g₂ : ConnectedComponents α → β<VAR>hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk<GOAL>g₁ = g₂
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TotallyDisconnectedSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>g : ConnectedComponents α → β<VAR>hg : g ∘ ConnectedComponents.mk = f<GOAL>g = h.connectedComponentsLift
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>Continuous h.connectedComponentsMap
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Y : Type u_3<VAR>TopologicalSpace Y<VAR>DiscreteTopology Y<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>f : α → Y<VAR>hf : ContinuousOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Y : Type u_3<VAR>TopologicalSpace Y<VAR>DiscreteTopology Y<VAR>hp : PreconnectedSpace α<VAR>f : α → Y<VAR>hf : Continuous f<VAR>x y : α<GOAL>f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : Set.MapsTo f S T<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : Set.MapsTo f S T<VAR>hne : T.Nonempty<GOAL>∃ y ∈ T, Set.EqOn f (Function.const α y) S
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : X ≃ₜ Y<GOAL>Continuous self.toFun
<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : X ≃ₜ Y<GOAL>Continuous self.invFun
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Function.Injective Homeomorph.toEquiv
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a : X ≃ Y<VAR>b : Continuous a.toFun<VAR>c : Continuous a.invFun<GOAL>⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c } = ⇑a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>h.symm.symm = h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Function.Bijective Homeomorph.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>⇑h.toEquiv = ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>⇑h.symm = ⇑h.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h h' : X ≃ₜ Y<VAR>H : ∀ (x : X), h x = h' x<GOAL>h = h'
<VAR>X : Type u_6<VAR>TopologicalSpace X<GOAL>⇑(Homeomorph.refl X) = id
<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>h₂ : Y ≃ₜ Z<VAR>x : X<GOAL>(h₁.trans h₂) x = h₂ (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>f : X ≃ₜ Y<VAR>g : Y ≃ₜ Z<VAR>z : Z<GOAL>(f.trans g).symm z = f.symm (g.symm z)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a : X ≃ Y<VAR>b : Continuous a.toFun<VAR>c : Continuous a.invFun<GOAL>⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c }.symm = ⇑a.symm
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(Homeomorph.refl X).symm = Homeomorph.refl X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Continuous ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Continuous ⇑h.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>y : Y<GOAL>h (h.symm y) = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>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<GOAL>h.trans h.symm = Homeomorph.refl X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>h.symm.trans h = Homeomorph.refl Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Function.Bijective ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Function.Injective ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Function.Surjective ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>⇑h.symm ∘ ⇑h = id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>⇑h ∘ ⇑h.symm = id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Set.range ⇑h = Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Set.image ⇑h.symm = Set.preimage ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Set.preimage ⇑h.symm = Set.image ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>⇑h '' (⇑h ⁻¹' s) = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h ⁻¹' (⇑h '' s) = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' sᶜ = (⇑h '' s)ᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Inducing ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>TopologicalSpace.induced (⇑h) inst✝ = inst✝¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>QuotientMap ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>TopologicalSpace.coinduced (⇑h) inst✝ = inst✝¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Embedding ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>SecondCountableTopology Y<VAR>h : X ≃ₜ Y<GOAL>SecondCountableTopology X
<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>IsCompact (⇑h '' s) ↔ IsCompact 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>IsCompact (⇑h ⁻¹' s) ↔ IsCompact s
<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>IsSigmaCompact (⇑h '' s) ↔ IsSigmaCompact 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>IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s
<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>IsPreconnected (⇑h '' s) ↔ IsPreconnected 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>IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s
<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>IsConnected (⇑h '' s) ↔ IsConnected 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>IsConnected (⇑h ⁻¹' s) ↔ IsConnected s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>h : X ≃ₜ Y<VAR>x : X<VAR>hx : x ∈ s<GOAL>⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Filter.comap (⇑h) (Filter.cocompact Y) = Filter.cocompact X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>Filter.map (⇑h) (Filter.cocompact X) = Filter.cocompact Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>h : X ≃ₜ Y<GOAL>CompactSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T0Space X<VAR>h : X ≃ₜ Y<GOAL>T0Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space X<VAR>h : X ≃ₜ Y<GOAL>T1Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>h : X ≃ₜ Y<GOAL>T2Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T3Space X<VAR>h : X ≃ₜ Y<GOAL>T3Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>DenseEmbedding ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>IsOpen (⇑h ⁻¹' s) ↔ IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>IsOpen (⇑h '' s) ↔ IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>IsOpenMap ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>IsClosed (⇑h ⁻¹' s) ↔ IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>IsClosed (⇑h '' s) ↔ IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>IsClosedMap ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>OpenEmbedding ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>ClosedEmbedding ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NormalSpace X<VAR>h : X ≃ₜ Y<GOAL>NormalSpace Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T4Space X<VAR>h : X ≃ₜ Y<GOAL>T4Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>⇑h ⁻¹' closure s = closure (⇑h ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' closure s = closure (⇑h '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>⇑h ⁻¹' interior s = interior (⇑h ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' interior s = interior (⇑h '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>⇑h ⁻¹' frontier s = frontier (⇑h ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' frontier s = frontier (⇑h '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>M : Type u_6<VAR>Zero M<VAR>f : Y → M<VAR>hf : HasCompactSupport f<VAR>φ : X ≃ₜ Y<GOAL>HasCompactSupport (f ∘ ⇑φ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>M : Type u_6<VAR>One M<VAR>f : Y → M<VAR>hf : HasCompactMulSupport f<VAR>φ : X ≃ₜ Y<GOAL>HasCompactMulSupport (f ∘ ⇑φ)
<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) (𝓝 x) = 𝓝 (h 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>Filter.map (⇑h) (𝓝[≠] x) = 𝓝[≠] h x