ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(spectrum R a), R)<VAR>hfg : f ≤ g<GOAL>(cfcHom ha) f ≤ (cfcHom ha) g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f : C(↑(spectrum R a), R)<GOAL>0 ≤ (cfcHom ha) f ↔ 0 ≤ f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ g x<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<GOAL>cfc f a ≤ cfc g a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a := by cfc_tac<GOAL>0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, 0 ≤ f x<GOAL>0 ≤ cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ 0<GOAL>cfc f a ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ r<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc f a ≤ (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, r ≤ f x<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>(algebraMap R A) r ≤ cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, x ≤ r<VAR>ha : p a := by cfc_tac<GOAL>a ≤ (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, r ≤ x<VAR>ha : p a := by cfc_tac<GOAL>(algebraMap R A) r ≤ a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ 1<GOAL>cfc f a ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommSemiring R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalSemiring R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, 1 ≤ f x<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>1 ≤ cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(spectrum R a), R)<GOAL>(cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>OrderedCommRing R<VAR>StarRing R<VAR>MetricSpace R<VAR>TopologicalRing R<VAR>ContinuousStar R<VAR>∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>TopologicalSpace A<VAR>Ring A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Algebra R A<VAR>ContinuousFunctionalCalculus R p<VAR>NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac<VAR>ha : p a := by cfc_tac<GOAL>cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>x ∈ intrinsicInterior 𝕜 s ↔ ∃ y ∈ interior (Subtype.val ⁻¹' s), ↑y = x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y ∈ frontier (Subtype.val ⁻¹' s), ↑y = x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>x : P<GOAL>x ∈ intrinsicClosure 𝕜 s ↔ ∃ y ∈ closure (Subtype.val ⁻¹' s), ↑y = x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicInterior 𝕜 s ⊆ s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>hs : IsClosed s<GOAL>intrinsicFrontier 𝕜 s ⊆ s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 s ⊆ intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>s ⊆ intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<GOAL>intrinsicInterior 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<GOAL>intrinsicFrontier 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<GOAL>intrinsicClosure 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>(intrinsicClosure 𝕜 s).Nonempty ↔ s.Nonempty
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>x : P<GOAL>intrinsicInterior 𝕜 {x} = {x}
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>x : P<GOAL>intrinsicFrontier 𝕜 {x} = ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>x : P<GOAL>intrinsicClosure 𝕜 {x} = {x}
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s t : Set P<VAR>h : s ⊆ t<GOAL>intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>interior s ⊆ intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 s ⊆ closure s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 s ⊆ frontier s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 s ⊆ ↑(affineSpan 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>hs : IsClosed ↑(affineSpan 𝕜 s)<GOAL>IsClosed (intrinsicClosure 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>hs : IsClosed ↑(affineSpan 𝕜 s)<GOAL>IsClosed (intrinsicFrontier 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>affineSpan 𝕜 (intrinsicClosure 𝕜 s) = affineSpan 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<VAR>hs : IsClosed (Subtype.val ⁻¹' s)<GOAL>intrinsicClosure 𝕜 s = s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>Ring 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>TopologicalSpace P<VAR>AddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>MetricSpace P<VAR>PseudoMetricSpace Q<VAR>NormedAddTorsor V P<VAR>NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>MetricSpace P<VAR>PseudoMetricSpace Q<VAR>NormedAddTorsor V P<VAR>NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>NormedField 𝕜<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>MetricSpace P<VAR>PseudoMetricSpace Q<VAR>NormedAddTorsor V P<VAR>NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>FiniteDimensional 𝕜 V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 s = closure s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>FiniteDimensional 𝕜 V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<GOAL>closure s \ intrinsicInterior 𝕜 s = intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>P : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>FiniteDimensional 𝕜 V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<GOAL>closure s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>φ : α ≃ₜ β<VAR>s : Set β<GOAL>(interior s).Nonempty ↔ (interior (⇑φ ⁻¹' s)).Nonempty
<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>s : Set V<VAR>hscv : Convex ℝ s<VAR>hsne : s.Nonempty<GOAL>(intrinsicInterior ℝ s).Nonempty
<VAR>V : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>s : Set V<VAR>hs : Convex ℝ s<GOAL>(intrinsicInterior ℝ s).Nonempty ↔ s.Nonempty
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>self : 𝓜(𝕜, A)<VAR>x y : A<GOAL>self.toProd.2 x * y = x * self.toProd.1 y
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<VAR>h : a.toProd = b.toProd<GOAL>a = b
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>Set.range DoubleCentralizer.toProd = {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>S : Type u_3<VAR>Monoid S<VAR>DistribMulAction S A<VAR>SMulCommClass 𝕜 S A<VAR>ContinuousConstSMul S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>s : S<VAR>a : 𝓜(𝕜, A)<GOAL>(s • a).toProd = s • a.toProd
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>S : Type u_3<VAR>Monoid S<VAR>DistribMulAction S A<VAR>SMulCommClass 𝕜 S A<VAR>ContinuousConstSMul S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>s : S<VAR>a : 𝓜(𝕜, A)<GOAL>(s • a).toProd.1 = s • a.toProd.1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>S : Type u_3<VAR>Monoid S<VAR>DistribMulAction S A<VAR>SMulCommClass 𝕜 S A<VAR>ContinuousConstSMul S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>s : S<VAR>a : 𝓜(𝕜, A)<GOAL>(s • a).toProd.2 = s • a.toProd.2
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a + b).toProd = a.toProd + b.toProd
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>DoubleCentralizer.toProd 0 = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>(-a).toProd = -a.toProd
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a - b).toProd = a.toProd - b.toProd
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>DoubleCentralizer.toProd 1 = 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<GOAL>(↑n).toProd = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℤ<GOAL>(↑n).toProd = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<VAR>a : 𝓜(𝕜, A)<GOAL>(a ^ n).toProd = a.toProd ^ n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a + b).toProd.1 = a.toProd.1 + b.toProd.1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a + b).toProd.2 = a.toProd.2 + b.toProd.2
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>(DoubleCentralizer.toProd 0).1 = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>(DoubleCentralizer.toProd 0).2 = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>(-a).toProd.1 = -a.toProd.1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>(-a).toProd.2 = -a.toProd.2
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a - b).toProd.1 = a.toProd.1 - b.toProd.1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a - b).toProd.2 = a.toProd.2 - b.toProd.2
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>(DoubleCentralizer.toProd 1).1 = 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>(DoubleCentralizer.toProd 1).2 = 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a * b).toProd.1 = a.toProd.1 * b.toProd.1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>a b : 𝓜(𝕜, A)<GOAL>(a * b).toProd.2 = b.toProd.2 * a.toProd.2
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<GOAL>(↑n).toProd.1 = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<GOAL>(↑n).toProd.2 = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℤ<GOAL>(↑n).toProd.1 = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℤ<GOAL>(↑n).toProd.2 = ↑n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<VAR>a : 𝓜(𝕜, A)<GOAL>(a ^ n).toProd.1 = a.toProd.1 ^ n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<VAR>n : ℕ<VAR>a : 𝓜(𝕜, A)<GOAL>(a ^ n).toProd.2 = a.toProd.2 ^ n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>Function.Injective DoubleCentralizer.toProdMulOpposite
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>SMulCommClass 𝕜 A A<VAR>IsScalarTower 𝕜 A A<GOAL>Set.range DoubleCentralizer.toProdMulOpposite = {lr | ∀ (x y : A), (MulOpposite.unop lr.2) x * y = x * lr.1 y}