ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>g : M₂ →L[R] M₃<VAR>f : ContinuousMultilinearMap R M₁ M₂<GOAL>⇑(g.compContinuousMultilinearMap f) = ⇑g ∘ ⇑f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>ι' : Type u_1<VAR>M' : ι' → Type u_2<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)<VAR>i : ι'<GOAL>ContinuousMultilinearMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>ι' : Type u_1<VAR>M' : ι' → Type u_2<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)<GOAL>ContinuousMultilinearMap.piEquiv f = ContinuousMultilinearMap.pi f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>ι' : Type u_1<VAR>e : ι ≃ ι'<VAR>f : ContinuousMultilinearMap R (fun x => M₂) M₃<GOAL>(ContinuousMultilinearMap.domDomCongr e f).toMultilinearMap = MultilinearMap.domDomCongr e f.toMultilinearMap
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>ι' : Type u_1<VAR>e : ι ≃ ι'<VAR>f : ContinuousMultilinearMap R (fun x => M₂) M₃<VAR>v : ι' → M₂<GOAL>(ContinuousMultilinearMap.domDomCongr e f) v = f fun i => v (e i)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>ι' : Type u_1<VAR>e : ι ≃ ι'<VAR>f : ContinuousMultilinearMap R (fun x => M₂) M₃<GOAL>(ContinuousMultilinearMap.domDomCongrEquiv e) f = ContinuousMultilinearMap.domDomCongr e f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>ι' : Type u_1<VAR>e : ι ≃ ι'<VAR>f : ContinuousMultilinearMap R (fun x => M₂) M₃<GOAL>(ContinuousMultilinearMap.domDomCongrEquiv e).symm f = ContinuousMultilinearMap.domDomCongr e.symm f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>ContinuousAdd M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>x y : (i : ι) → M₁ i<GOAL>(f.linearDeriv x) y = ∑ i : ι, f (Function.update x i (y i))
<VAR>R : Type u<VAR>n : ℕ<VAR>M : Fin n.succ → Type w<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>(i : Fin n.succ) → TopologicalSpace (M i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.succ<VAR>x y : M 0<GOAL>f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
<VAR>R : Type u<VAR>n : ℕ<VAR>M : Fin n.succ → Type w<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : Fin n.succ) → AddCommMonoid (M i)<VAR>AddCommMonoid M₂<VAR>(i : Fin n.succ) → Module R (M i)<VAR>Module R M₂<VAR>(i : Fin n.succ) → TopologicalSpace (M i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.succ<VAR>c : R<VAR>x : M 0<GOAL>f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m m' : (i : ι) → M₁ i<VAR>t : Finset ι<GOAL>f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m m' : (i : ι) → M₁ i<GOAL>f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>Fintype ι<VAR>g : (i : ι) → α i → M₁ i<VAR>A : (i : ι) → Finset (α i)<VAR>DecidableEq ι<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<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>α : ι → Type u_1<VAR>Fintype ι<VAR>g : (i : ι) → α i → M₁ i<VAR>DecidableEq ι<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<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>A : Type u_1<VAR>Semiring A<VAR>SMul R A<VAR>(i : ι) → Module A (M₁ i)<VAR>Module A M₂<VAR>∀ (i : ι), IsScalarTower R A (M₁ i)<VAR>IsScalarTower R A M₂<VAR>f : ContinuousMultilinearMap A M₁ M₂<GOAL>⇑(ContinuousMultilinearMap.restrictScalars R f) = ⇑f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Ring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x y : M₁ i<GOAL>f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Ring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>TopologicalAddGroup M₂<VAR>m : (i : ι) → M₁ i<GOAL>(-f) m = -f m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Ring R<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>AddCommGroup M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f f' : ContinuousMultilinearMap R M₁ M₂<VAR>TopologicalAddGroup M₂<VAR>m : (i : ι) → M₁ i<GOAL>(f - f') m = f m - f' m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>Fintype ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<GOAL>(f fun i => c i • m i) = (∏ i : ι, c i) • f m
<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>R' : Type u_1<VAR>A : Type u_2<VAR>Semiring R'<VAR>Semiring A<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>ContinuousAdd M₂<VAR>(i : ι) → Module A (M₁ i)<VAR>Module A M₂<VAR>Module R' M₂<VAR>ContinuousConstSMul R' M₂<VAR>SMulCommClass A R' M₂<VAR>self : ContinuousMultilinearMap A M₁ M₂<GOAL>ContinuousMultilinearMap.toMultilinearMapLinear self = self.toMultilinearMap
<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>R' : Type u_1<VAR>A : Type u_2<VAR>Semiring R'<VAR>Semiring A<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>(i : ι) → Module A (M₁ i)<VAR>ι' : Type u_3<VAR>M' : ι' → Type u_4<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 : ι') → ContinuousMultilinearMap A M₁ (M' i)), ContinuousMultilinearMap.piLinearEquiv a = ContinuousMultilinearMap.pi a
<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>R' : Type u_1<VAR>A : Type u_2<VAR>Semiring R'<VAR>Semiring A<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>(i : ι) → Module A (M₁ i)<VAR>ι' : Type u_3<VAR>M' : ι' → Type u_4<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 : ContinuousMultilinearMap A M₁ ((i : ι') → M' i)) (i : ι'), ContinuousMultilinearMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap a
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type u_1<VAR>Fintype ι<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>ContinuousMul A<VAR>m : ι → A<GOAL>(ContinuousMultilinearMap.mkPiAlgebra R ι A) m = ∏ i : ι, m i
<VAR>R : Type u<VAR>n : ℕ<VAR>A : Type u_1<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>ContinuousMul A<VAR>m : Fin n → A<GOAL>(ContinuousMultilinearMap.mkPiAlgebraFin R n A) m = (List.ofFn m).prod
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>TopologicalSpace R<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>ContinuousSMul R M₂<VAR>f : ContinuousMultilinearMap R M₁ R<VAR>z : M₂<GOAL>∀ (a : (i : ι) → M₁ i), (f.smulRight z) a = f a • z
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>TopologicalSpace R<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>ContinuousSMul R M₂<VAR>f : ContinuousMultilinearMap R M₁ R<VAR>z : M₂<GOAL>(f.smulRight z).toMultilinearMap = f.smulRight z
<VAR>R : Type u<VAR>ι : Type v<VAR>M : Type u_1<VAR>Fintype ι<VAR>CommRing R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>ContinuousMul R<VAR>ContinuousSMul R M<VAR>z : M<VAR>m : ι → R<GOAL>(ContinuousMultilinearMap.mkPiRing R ι z) m = (∏ i : ι, m i) • z
<VAR>R : Type u<VAR>ι : Type v<VAR>M : Type u_1<VAR>Fintype ι<VAR>CommRing R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>ContinuousMul R<VAR>ContinuousSMul R M<VAR>f : ContinuousMultilinearMap R (fun x => R) M<GOAL>ContinuousMultilinearMap.mkPiRing R ι (f fun x => 1) = f
<VAR>R : Type u<VAR>ι : Type v<VAR>M : Type u_1<VAR>Fintype ι<VAR>CommRing R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>ContinuousMul R<VAR>ContinuousSMul R M<VAR>z₁ z₂ : M<GOAL>ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
<VAR>R : Type u<VAR>ι : Type v<VAR>M : Type u_1<VAR>Fintype ι<VAR>CommRing R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>ContinuousMul R<VAR>ContinuousSMul R M<GOAL>ContinuousMultilinearMap.mkPiRing R ι 0 = 0
<VAR>R : Type u<VAR>ι : Type v<VAR>M : Type u_1<VAR>Fintype ι<VAR>CommRing R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>ContinuousMul R<VAR>ContinuousSMul R M<VAR>z : M<GOAL>ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
<VAR>R : Type u_1<VAR>TopologicalSpace R<VAR>Ring R<VAR>TopologicalRing R<VAR>I : Ideal R<GOAL>↑I.closure = closure ↑I
<VAR>R : Type u_1<VAR>TopologicalSpace R<VAR>Ring R<VAR>TopologicalRing R<VAR>I : Ideal R<VAR>hI : IsClosed ↑I<GOAL>I.closure = I
<VAR>R : Type u_1<VAR>TopologicalSpace R<VAR>CommRing R<VAR>N : Ideal R<VAR>TopologicalRing R<GOAL>IsOpenMap ⇑(Ideal.Quotient.mk N)
<VAR>R : Type u_1<VAR>TopologicalSpace R<VAR>CommRing R<VAR>N : Ideal R<VAR>TopologicalRing R<GOAL>QuotientMap fun p => ((Ideal.Quotient.mk N) p.1, (Ideal.Quotient.mk N) p.2)
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous AddOpposite.unop
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous MulOpposite.unop
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous AddOpposite.op
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Continuous MulOpposite.op
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>∀ (a : M), AddOpposite.opHomeomorph a = AddOpposite.op a
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>∀ (a : M), MulOpposite.opHomeomorph a = MulOpposite.op a
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>∀ (a : Mᵐᵒᵖ), MulOpposite.opHomeomorph.symm a = MulOpposite.unop a
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>∀ (a : Mᵃᵒᵖ), AddOpposite.opHomeomorph.symm a = AddOpposite.unop a
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.map AddOpposite.op (𝓝 x) = 𝓝 (AddOpposite.op x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.map MulOpposite.op (𝓝 x) = 𝓝 (MulOpposite.op x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵃᵒᵖ<GOAL>Filter.map AddOpposite.unop (𝓝 x) = 𝓝 (AddOpposite.unop x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵐᵒᵖ<GOAL>Filter.map MulOpposite.unop (𝓝 x) = 𝓝 (MulOpposite.unop x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵃᵒᵖ<GOAL>Filter.comap AddOpposite.op (𝓝 x) = 𝓝 (AddOpposite.unop x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵐᵒᵖ<GOAL>Filter.comap MulOpposite.op (𝓝 x) = 𝓝 (MulOpposite.unop x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.comap MulOpposite.unop (𝓝 x) = 𝓝 (MulOpposite.op x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.comap AddOpposite.unop (𝓝 x) = 𝓝 (AddOpposite.op x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>Inducing ⇑(AddUnits.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Inducing ⇑(Units.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>Embedding ⇑(AddUnits.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Embedding ⇑(Units.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Units.instTopologicalSpaceUnits = TopologicalSpace.induced Units.val inst✝ ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst✝
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>AddUnits.instTopologicalSpaceAddUnits = TopologicalSpace.induced AddUnits.val inst✝ ⊓ TopologicalSpace.induced (fun u => ↑(-u)) inst✝
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsAddUnit x}<VAR>hf : ∀ (u : AddUnits M), f ↑u = ↑(-u)<GOAL>Embedding AddUnits.val
<VAR>M : Type u_3<VAR>Monoid M<VAR>TopologicalSpace M<VAR>f : M → M<VAR>hc : ContinuousOn f {x | IsUnit x}<VAR>hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹<GOAL>Embedding Units.val
<VAR>M : Type u_3<VAR>DivisionMonoid M<VAR>TopologicalSpace M<VAR>h : ContinuousOn Inv.inv {x | IsUnit x}<GOAL>Embedding Units.val
<VAR>M : Type u_3<VAR>SubtractionMonoid M<VAR>TopologicalSpace M<VAR>h : ContinuousOn Neg.neg {x | IsAddUnit x}<GOAL>Embedding AddUnits.val
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>Continuous ⇑(AddUnits.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Continuous ⇑(Units.embedProduct M)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Continuous Units.val
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>Continuous AddUnits.val
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>Monoid M<VAR>TopologicalSpace X<VAR>f : X → Mˣ<GOAL>Continuous f ↔ Continuous (Units.val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace M<VAR>AddMonoid M<VAR>TopologicalSpace X<VAR>f : X → AddUnits M<GOAL>Continuous f ↔ Continuous (AddUnits.val ∘ f) ∧ Continuous fun x => ↑(-f x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>AddMonoid M<GOAL>Continuous fun u => ↑(-u)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>Monoid M<GOAL>Continuous fun u => ↑u⁻¹
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>HasSeparatingCover ∅ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>HasSeparatingCover s ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s₁ s₂ t₁ t₂ : Set X<VAR>sc_st : HasSeparatingCover s₂ t₂<VAR>s_sub : s₁ ⊆ s₂<VAR>t_sub : t₁ ⊆ t₂<GOAL>HasSeparatingCover s₁ t₁
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>SeparatedNhds s t → SeparatedNhds t s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<GOAL>SeparatedNhds s t ↔ SeparatedNhds t s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s t : Set Y<VAR>h : SeparatedNhds s t<VAR>hf : Continuous f<GOAL>SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : SeparatedNhds s t<GOAL>Disjoint s t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : SeparatedNhds s t<GOAL>Disjoint (closure s) t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>h : SeparatedNhds s t<GOAL>Disjoint s (closure t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>SeparatedNhds s ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>SeparatedNhds ∅ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s₁ s₂ t₁ t₂ : Set X<VAR>h : SeparatedNhds s₂ t₂<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<GOAL>SeparatedNhds s₁ t₁
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t u : Set X<GOAL>SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t u : Set X<VAR>ht : SeparatedNhds s t<VAR>hu : SeparatedNhds s u<GOAL>SeparatedNhds s (t ∪ u)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : T0Space X<VAR>x y : X<GOAL>Inseparable x y → x = y
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T0Space X ↔ ∀ (x y : X), Inseparable x y → x = y
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun x y => ¬Inseparable x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>x y : X<VAR>h : Inseparable x y<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T0Space X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>Function.Injective f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T0Space X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>Embedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T0Space X<VAR>f : X → Y<GOAL>Embedding f ↔ Inducing f
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T0Space X ↔ Function.Injective 𝓝
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<GOAL>Function.Injective 𝓝
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>x y : X<GOAL>Inseparable x y ↔ x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>a b : X<GOAL>𝓝 a = 𝓝 b ↔ a = b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<GOAL>Inseparable = Eq
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>b : Set (Set X)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>x y : X<GOAL>Inseparable x y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>b : Set (Set X)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>x y : X<GOAL>x = y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<GOAL>s.Subsingleton
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<GOAL>∃ x, s = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<GOAL>∃ x ∈ S, IsClosed {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<GOAL>s.Subsingleton
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hne : s.Nonempty<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s<GOAL>∃ x, s = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>s : Set X<VAR>hfin : s.Finite<VAR>hne : s.Nonempty<VAR>ho : IsOpen s<GOAL>∃ x ∈ s, IsOpen {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T0Space X<VAR>Finite X<VAR>Nonempty X<GOAL>∃ x, IsOpen {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Function.Injective f<VAR>hf' : Continuous f<VAR>T0Space Y<GOAL>T0Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T0Space Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>T0Space X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun a b => a ∉ closure {b} ∨ b ∉ closure {a}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s<GOAL>T0Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>h : ∀ (x : X), ∃ s, x ∈ s ∧ IsOpen s ∧ T0Space ↑s<GOAL>T0Space X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : R0Space X<GOAL>Symmetric Specializes
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>R0Space X ↔ Symmetric Specializes
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>x y : X<VAR>h : x ⤳ y<GOAL>y ⤳ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>x y : X<GOAL>x ⤳ y ↔ y ⤳ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>x y : X<GOAL>x ⤳ y ↔ Inseparable x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R0Space X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<GOAL>R0Space Y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>x : X<GOAL>IsCompact (closure {x})
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<GOAL>Filter.coclosedCompact X ≤ Filter.cofinite
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>s : Set X<GOAL>Bornology.IsBounded s ↔ IsCompact (closure s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R0Space X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsCompact (closure s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : T1Space X<VAR>x : X<GOAL>IsClosed {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<GOAL>IsClosed {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<GOAL>IsOpen {x}ᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<GOAL>IsOpen {y | y ≠ x}