ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Embedding ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>OpenEmbedding ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>OpenEmbedding ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>ClosedEmbedding ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>ClosedEmbedding ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>QuotientMap ⇑DomAddAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>QuotientMap ⇑DomMulAct.mk
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Inducing ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Inducing ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Embedding ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>Embedding ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>OpenEmbedding ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>OpenEmbedding ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>ClosedEmbedding ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>ClosedEmbedding ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>QuotientMap ⇑DomMulAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<GOAL>QuotientMap ⇑DomAddAct.mk.symm
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.map (⇑DomAddAct.mk) (𝓝 x) = 𝓝 (DomAddAct.mk x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.map (⇑DomMulAct.mk) (𝓝 x) = 𝓝 (DomMulAct.mk x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵈᵐᵃ<GOAL>Filter.map (⇑DomMulAct.mk.symm) (𝓝 x) = 𝓝 (DomMulAct.mk.symm x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵈᵃᵃ<GOAL>Filter.map (⇑DomAddAct.mk.symm) (𝓝 x) = 𝓝 (DomAddAct.mk.symm x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵈᵐᵃ<GOAL>Filter.comap (⇑DomMulAct.mk) (𝓝 x) = 𝓝 (DomMulAct.mk.symm x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : Mᵈᵃᵃ<GOAL>Filter.comap (⇑DomAddAct.mk) (𝓝 x) = 𝓝 (DomAddAct.mk.symm x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.comap (⇑DomAddAct.mk.symm) (𝓝 x) = 𝓝 (DomAddAct.mk x)
<VAR>M : Type u_1<VAR>TopologicalSpace M<VAR>x : M<GOAL>Filter.comap (⇑DomMulAct.mk.symm) (𝓝 x) = 𝓝 (DomMulAct.mk x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Zero Y<GOAL>⇑0 = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>One Y<GOAL>⇑1 = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Zero Y<VAR>x : X<GOAL>0 x = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>One Y<VAR>x : X<GOAL>1 x = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Neg Y<VAR>f : LocallyConstant X Y<GOAL>⇑(-f) = -⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Inv Y<VAR>f : LocallyConstant X Y<GOAL>⇑f⁻¹ = (⇑f)⁻¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Neg Y<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>(-f) x = -f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Inv Y<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>f⁻¹ x = (f x)⁻¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Add Y<VAR>f g : LocallyConstant X Y<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Mul Y<VAR>f g : LocallyConstant X Y<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Mul Y<VAR>f g : LocallyConstant X Y<VAR>x : X<GOAL>(f * g) x = f x * g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Add Y<VAR>f g : LocallyConstant X Y<VAR>x : X<GOAL>(f + g) x = f x + g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulOneClass Y<GOAL>∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnMonoidHom a a_1 = a a_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>AddZeroClass Y<GOAL>∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnAddMonoidHom a a_1 = a a_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulOneClass Y<VAR>y : Y<GOAL>LocallyConstant.constMonoidHom y = LocallyConstant.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>AddZeroClass Y<VAR>y : Y<GOAL>LocallyConstant.constAddMonoidHom y = LocallyConstant.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulZeroOneClass Y<VAR>U : Set X<VAR>hU : IsClopen U<GOAL>⇑(LocallyConstant.charFn Y hU) = U.indicator 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulZeroOneClass Y<VAR>U : Set X<VAR>Nontrivial Y<VAR>x : X<VAR>hU : IsClopen U<GOAL>(LocallyConstant.charFn Y hU) x = 1 ↔ x ∈ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulZeroOneClass Y<VAR>U : Set X<VAR>Nontrivial Y<VAR>x : X<VAR>hU : IsClopen U<GOAL>(LocallyConstant.charFn Y hU) x = 0 ↔ x ∉ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulZeroOneClass Y<VAR>U V : Set X<VAR>Nontrivial Y<VAR>hU : IsClopen U<VAR>hV : IsClopen V<VAR>h : LocallyConstant.charFn Y hU = LocallyConstant.charFn Y hV<GOAL>U = V
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Div Y<VAR>f g : LocallyConstant X Y<GOAL>⇑(f / g) = ⇑f / ⇑g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Sub Y<VAR>f g : LocallyConstant X Y<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Sub Y<VAR>f g : LocallyConstant X Y<VAR>x : X<GOAL>(f - g) x = f x - g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Div Y<VAR>f g : LocallyConstant X Y<VAR>x : X<GOAL>(f / g) x = f x / g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_4<VAR>SMul R Y<VAR>r : R<VAR>f : LocallyConstant X Y<GOAL>⇑(r • f) = r • ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_4<VAR>VAdd R Y<VAR>r : R<VAR>f : LocallyConstant X Y<GOAL>⇑(r +ᵥ f) = r +ᵥ ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_4<VAR>VAdd R Y<VAR>r : R<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>(r +ᵥ f) x = r +ᵥ f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_4<VAR>SMul R Y<VAR>r : R<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>(r • f) x = r • f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>NonAssocSemiring Y<VAR>y : Y<GOAL>LocallyConstant.constRingHom y = LocallyConstant.const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>r : R<GOAL>⇑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R (X → Y)) r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Semiring Y<GOAL>∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnRingHom a a_1 = a a_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<GOAL>∀ (a : LocallyConstant X Y) (a_1 : X), (LocallyConstant.coeFnₗ R) a a_1 = a a_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<GOAL>∀ (a : LocallyConstant X Y) (a_1 : X), (LocallyConstant.coeFnAlgHom R) a a_1 = a a_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>AddZeroClass Y<VAR>x : X<GOAL>∀ (a : LocallyConstant X Y), (LocallyConstant.evalAddMonoidHom x) a = a x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>MulOneClass Y<VAR>x : X<GOAL>∀ (a : LocallyConstant X Y), (LocallyConstant.evalMonoidHom x) a = a x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>x : X<GOAL>∀ (a : LocallyConstant X Y), (LocallyConstant.evalₗ R x) a = a x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Semiring Y<VAR>x : X<GOAL>∀ (a : LocallyConstant X Y), (LocallyConstant.evalRingHom x) a = a x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>x : X<GOAL>∀ (a : LocallyConstant X Y), (LocallyConstant.evalₐ R x) a = a x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>AddZeroClass Z<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>(LocallyConstant.comapAddMonoidHom f) g = LocallyConstant.comap f g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>MulOneClass Z<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>(LocallyConstant.comapMonoidHom f) g = LocallyConstant.comap f g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>∀ (a : X), ((LocallyConstant.comapₗ R f) g) a = g (f a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>Semiring Z<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>∀ (a : X), ((LocallyConstant.comapRingHom f) g) a = g (f a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Z<VAR>Algebra R Z<VAR>f : C(X, Y)<VAR>g : LocallyConstant Y Z<GOAL>∀ (a : X), ((LocallyConstant.comapₐ R f) g) a = g (f a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_5<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>Semiring R<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>f : C(X, Y)<VAR>hfs : Function.Surjective ⇑f<GOAL>LinearMap.ker (LocallyConstant.comapₗ R f) = ⊥
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>e : X ≃ₜ Y<GOAL>∀ (a : LocallyConstant Y Z) (a_1 : X), ((LocallyConstant.congrLeftₗ R e).symm a) a_1 = a (e a_1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant X Z<GOAL>∀ (a : Y), ((LocallyConstant.congrLeftₗ R e) g) a = g (e.symm a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>Semiring Z<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant X Z<GOAL>∀ (a : Y), ((LocallyConstant.congrLeftRingEquiv e) g) a = g (e.symm a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>Semiring Z<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant Y Z<GOAL>∀ (a : X), ((LocallyConstant.congrLeftRingEquiv e).symm g) a = g (e a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Z<VAR>Algebra R Z<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant X Z<GOAL>∀ (a : Y), ((LocallyConstant.congrLeftₐ R e) g) a = g (e.symm a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Z<VAR>Algebra R Z<VAR>e : X ≃ₜ Y<VAR>g : LocallyConstant Y Z<GOAL>∀ (a : X), ((LocallyConstant.congrLeftₐ R e).symm g) a = g (e a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>MulOneClass Y<VAR>MulOneClass Z<VAR>f : Y →* Z<VAR>g : LocallyConstant X Y<GOAL>(LocallyConstant.mapMonoidHom f) g = LocallyConstant.map (⇑f) g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>AddZeroClass Y<VAR>AddZeroClass Z<VAR>f : Y →+ Z<VAR>g : LocallyConstant X Y<GOAL>(LocallyConstant.mapAddMonoidHom f) g = LocallyConstant.map (⇑f) g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>f : Y →ₗ[R] Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.mapₗ R f) g) a = f (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>Semiring Y<VAR>Semiring Z<VAR>f : Y →+* Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.mapRingHom f) g) a = f (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>Semiring Z<VAR>Algebra R Z<VAR>f : Y →ₐ[R] Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.mapₐ R f) g) a = f (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>e : Y ≃ₗ[R] Z<GOAL>∀ (a : LocallyConstant X Z) (a_1 : X), ((LocallyConstant.congrRightₗ R e).symm a) a_1 = e.symm (a a_1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>AddCommMonoid Z<VAR>Module R Z<VAR>e : Y ≃ₗ[R] Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.congrRightₗ R e) g) a = e (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>Semiring Y<VAR>Semiring Z<VAR>e : Y ≃+* Z<VAR>g : LocallyConstant X Z<GOAL>∀ (a : X), ((LocallyConstant.congrRightRingEquiv e).symm g) a = (↑e).symm (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>Semiring Y<VAR>Semiring Z<VAR>e : Y ≃+* Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.congrRightRingEquiv e) g) a = e (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>Semiring Z<VAR>Algebra R Z<VAR>e : Y ≃ₐ[R] Z<VAR>g : LocallyConstant X Y<GOAL>∀ (a : X), ((LocallyConstant.congrRightₐ R e) g) a = e (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_6<VAR>R : Type u_7<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>Semiring Z<VAR>Algebra R Z<VAR>e : Y ≃ₐ[R] Z<VAR>g : LocallyConstant X Z<GOAL>∀ (a : X), ((LocallyConstant.congrRightₐ R e).symm g) a = e.symm (g a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>Semiring R<VAR>AddCommMonoid Y<VAR>Module R Y<VAR>y : Y<GOAL>∀ (a : X), ((LocallyConstant.constₗ R) y) a = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R : Type u_6<VAR>CommSemiring R<VAR>Semiring Y<VAR>Algebra R Y<VAR>y : Y<GOAL>∀ (a : X), ((LocallyConstant.constₐ R) y) a = y
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>T2Space R<VAR>s : Set X<GOAL>IsClosed ↑(ContinuousMap.idealOfSet R s)
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>f ∈ ContinuousMap.idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>f ∉ ContinuousMap.idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>x ∉ ContinuousMap.setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>I : Ideal C(X, R)<VAR>x : X<GOAL>x ∈ ContinuousMap.setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>T2Space R<VAR>I : Ideal C(X, R)<GOAL>IsOpen (ContinuousMap.setOfIdeal I)
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>T2Space R<VAR>I : Ideal C(X, R)<GOAL>↑(ContinuousMap.opensOfIdeal I) = ContinuousMap.setOfIdeal I
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>Nontrivial R<GOAL>ContinuousMap.setOfIdeal ⊤ = Set.univ
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<GOAL>ContinuousMap.idealOfSet R ∅ = ⊥
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>x : X<VAR>f : C(X, R)<GOAL>f ∈ ContinuousMap.idealOfSet R {x}ᶜ ↔ f x = 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>TopologicalSpace X<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<GOAL>GaloisConnection ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet R)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : C(X, ℝ≥0)<VAR>c : ℝ≥0<VAR>hc : 0 < c<GOAL>∃ g, (∀ (x : X), (g * f) x ≤ 1) ∧ Set.EqOn (⇑(g * f)) 1 {x | c ≤ f x}
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>I : Ideal C(X, 𝕜)<GOAL>ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I.closure
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<GOAL>ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>s : Set X<GOAL>ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = interior s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>I : Ideal C(X, 𝕜)<GOAL>∀ (x : ContinuousMap.idealOfSet 𝕜 ↑(ContinuousMap.opensOfIdeal I) ≤ I), (ContinuousMap.idealOpensGI X 𝕜).choice I x = ContinuousMap.opensOfIdeal I.closure
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>s : TopologicalSpace.Opens X<GOAL>(ContinuousMap.idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>x : X<GOAL>(ContinuousMap.idealOfSet 𝕜 {x}ᶜ).IsMaximal
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : I.IsMaximal<GOAL>∃ x, ContinuousMap.setOfIdeal I = {x}ᶜ
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<GOAL>I.IsMaximal ↔ ∃ x, ContinuousMap.idealOfSet 𝕜 {x}ᶜ = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>TopologicalSpace X<VAR>CommRing 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>Nontrivial 𝕜<VAR>NoZeroDivisors 𝕜<VAR>x : X<VAR>f : C(X, 𝕜)<GOAL>((WeakDual.CharacterSpace.continuousMapEval X 𝕜) x) f = f x
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>T2Space X<VAR>RCLike 𝕜<GOAL>Function.Bijective ⇑(WeakDual.CharacterSpace.continuousMapEval X 𝕜)
<VAR>G : Type u<VAR>Group G<VAR>self : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ GroupFilterBasis.toFilterBasis.sets → ∃ V ∈ GroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x⁻¹) ⁻¹' U
<VAR>G : Type u<VAR>Group G<VAR>self : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ GroupFilterBasis.toFilterBasis.sets → 1 ∈ U
<VAR>G : Type u<VAR>Group G<VAR>self : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ GroupFilterBasis.toFilterBasis.sets → ∃ V ∈ GroupFilterBasis.toFilterBasis.sets, V * V ⊆ U
<VAR>G : Type u<VAR>Group G<VAR>self : GroupFilterBasis G<VAR>x₀ : G<VAR>U : Set G<GOAL>U ∈ GroupFilterBasis.toFilterBasis.sets → ∃ V ∈ GroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
<VAR>A : Type u<VAR>AddGroup A<VAR>self : AddGroupFilterBasis A<VAR>x₀ : A<VAR>U : Set A<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
<VAR>A : Type u<VAR>AddGroup A<VAR>self : AddGroupFilterBasis A<VAR>U : Set A<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V + V ⊆ U
<VAR>A : Type u<VAR>AddGroup A<VAR>self : AddGroupFilterBasis A<VAR>U : Set A<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => -x) ⁻¹' U
<VAR>A : Type u<VAR>AddGroup A<VAR>self : AddGroupFilterBasis A<VAR>U : Set A<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → 0 ∈ U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → 1 ∈ U
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → 0 ∈ U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V * V ⊆ U
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V + V ⊆ U
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V ⊆ (fun x => -x) ⁻¹' U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x⁻¹) ⁻¹' U
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>x₀ : G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>x₀ : G<VAR>U : Set G<GOAL>U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>U : Set G<VAR>h : U ∈ B<GOAL>U ⊆ U + U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>U : Set G<VAR>h : U ∈ B<GOAL>U ⊆ U * U
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<GOAL>B.N 1 = GroupFilterBasis.toFilterBasis.filter
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<GOAL>B.N 0 = AddGroupFilterBasis.toFilterBasis.filter
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>x : G<GOAL>(B.N x).HasBasis (fun V => V ∈ B) fun V => (fun y => x * y) '' V
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>x : G<GOAL>(B.N x).HasBasis (fun V => V ∈ B) fun V => (fun y => x + y) '' V
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>x₀ : G<GOAL>𝓝 x₀ = B.N x₀
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>x₀ : G<GOAL>𝓝 x₀ = B.N x₀
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<GOAL>𝓝 1 = GroupFilterBasis.toFilterBasis.filter
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<GOAL>𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>x₀ : G<GOAL>(𝓝 x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ * y) '' V
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>x₀ : G<GOAL>(𝓝 x₀).HasBasis (fun V => V ∈ B) fun V => (fun y => x₀ + y) '' V
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<GOAL>(𝓝 0).HasBasis (fun V => V ∈ B) id
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<GOAL>(𝓝 1).HasBasis (fun V => V ∈ B) id
<VAR>G : Type u<VAR>Group G<VAR>B : GroupFilterBasis G<VAR>U : Set G<VAR>hU : U ∈ B<GOAL>U ∈ 𝓝 1
<VAR>G : Type u<VAR>AddGroup G<VAR>B : AddGroupFilterBasis G<VAR>U : Set G<VAR>hU : U ∈ B<GOAL>U ∈ 𝓝 0
<VAR>R : Type u<VAR>Ring R<VAR>self : RingFilterBasis R<VAR>U : Set R<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V * V ⊆ U
<VAR>R : Type u<VAR>Ring R<VAR>self : RingFilterBasis R<VAR>x₀ : R<VAR>U : Set R<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x * x₀) ⁻¹' U
<VAR>R : Type u<VAR>Ring R<VAR>self : RingFilterBasis R<VAR>x₀ : R<VAR>U : Set R<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x₀ * x) ⁻¹' U
<VAR>R : Type u<VAR>Ring R<VAR>B : RingFilterBasis R<VAR>U : Set R<VAR>hU : U ∈ B<GOAL>∃ V ∈ B, V * V ⊆ U
<VAR>R : Type u<VAR>Ring R<VAR>B : RingFilterBasis R<VAR>x₀ : R<VAR>U : Set R<VAR>hU : U ∈ B<GOAL>∃ V ∈ B, V ⊆ (fun x => x₀ * x) ⁻¹' U
<VAR>R : Type u<VAR>Ring R<VAR>B : RingFilterBasis R<VAR>x₀ : R<VAR>U : Set R<VAR>hU : U ∈ B<GOAL>∃ V ∈ B, V ⊆ (fun x => x * x₀) ⁻¹' U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>TopologicalSpace R<VAR>AddCommGroup M<VAR>Module R M<VAR>self : ModuleFilterBasis R M<VAR>x₀ : R<VAR>U : Set M<GOAL>U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U