theorem
IsCompact.sSup_image_eq_sSup_image_closure
{α : Type u_1}
{β : Type u_2}
{S : Set β}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
{f : β → α}
(hS : IsCompact (closure S))
(hf : Continuous f)
:
theorem
IsCompact.sInf_image_eq_sInf_image_closure
{α : Type u_1}
{β : Type u_2}
{S : Set β}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
{f : β → α}
(hS : IsCompact (closure S))
(hf : Continuous f)
:
theorem
IsCompact.closure_continuous_sSup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[TopologicalSpace β]
(hS : IsCompact (closure S))
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => sSup (f x '' S)
A version of IsCompact.continuous_sSup with a slightly weaker hypothesis on the set K,
that its closure is compact (but the set itself need not be).
theorem
IsCompact.closure_continuous_sInf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[TopologicalSpace β]
(hS : IsCompact (closure S))
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => sInf (f x '' S)
A version of IsCompact.continuous_sInf with a slightly weaker hypothesis on the set K,
that its closure is compact (but the set itself need not be).
theorem
IsCompact.continuous_iSup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[TopologicalSpace β]
(hS : IsCompact (closure S))
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => ⨆ (y : ↑S), f x ↑y
theorem
IsCompact.continuous_iInf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[TopologicalSpace β]
(hS : IsCompact (closure S))
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => ⨅ (y : ↑S), f x ↑y
theorem
Bornology.IsBounded.continuous_sSup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[PseudoMetricSpace β]
[ProperSpace β]
(hS : IsBounded S)
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => sSup (f x '' S)
Similar to IsCompact.continuous_sSup, but taking a bounded set in the bornology instead
of a compact set.
theorem
Bornology.IsBounded.continuous_sInf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[PseudoMetricSpace β]
[ProperSpace β]
(hS : IsBounded S)
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => sInf (f x '' S)
Similar to IsCompact.continuous_sInf, but taking a bounded set in the bornology instead
of a compact set.
theorem
Bornology.IsBounded.continuous_iSup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[PseudoMetricSpace β]
[ProperSpace β]
(hS : IsBounded S)
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => ⨆ (y : ↑S), f x ↑y
theorem
Bornology.IsBounded.continuous_iInf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{S : Set β}
{f : γ → β → α}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace γ]
[PseudoMetricSpace β]
[ProperSpace β]
(hS : IsBounded S)
(hf : Continuous ↿f)
:
Continuous fun (x : γ) => ⨅ (y : ↑S), f x ↑y
theorem
LinearMap.continuous_iSup
{E : Type u_4}
{F : Type u_5}
{𝕜 : Type u_6}
[CommRing 𝕜]
[TopologicalSpace 𝕜]
[IsTopologicalRing 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[AddCommGroup E]
[TopologicalSpace E]
[Module 𝕜 E]
[IsModuleTopology 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[PseudoMetricSpace F]
[ProperSpace F]
[Module.Finite 𝕜 F]
[IsModuleTopology 𝕜 F]
(f : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{S : Set F}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨆ (y : ↑S), (f x) ↑y
For bilinear maps in suitably well-behaved spaces with IsModuleTopology, taking the supremum in one
argument is still Continuous, by Bornology.IsBounded.continuous_iSup.
theorem
LinearMap.continuous_iInf
{E : Type u_4}
{F : Type u_5}
{𝕜 : Type u_6}
[CommRing 𝕜]
[TopologicalSpace 𝕜]
[IsTopologicalRing 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[AddCommGroup E]
[TopologicalSpace E]
[Module 𝕜 E]
[IsModuleTopology 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[PseudoMetricSpace F]
[ProperSpace F]
[Module.Finite 𝕜 F]
[IsModuleTopology 𝕜 F]
(f : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{S : Set F}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨅ (y : ↑S), (f x) ↑y
For bilinear maps in suitably well-behaved spaces with IsModuleTopology, taking the infimum in one
argument is still Continuous, by Bornology.IsBounded.continuous_iInf.
theorem
LinearMap.continuous_iSup'
{E : Type u_4}
{F : Type u_5}
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[CompleteSpace 𝕜]
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[T2Space E]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[FiniteDimensional 𝕜 E]
[PseudoMetricSpace F]
[ProperSpace F]
[AddCommGroup F]
[IsTopologicalAddGroup F]
[T2Space F]
[Module 𝕜 F]
[ContinuousSMul 𝕜 F]
[FiniteDimensional 𝕜 F]
(f : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{S : Set F}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨆ (y : ↑S), (f x) ↑y
A specialization of LinearMap.continuous_iSup to finite dimensional spaces, in place
of requiring a (non-instance) IsModuleTopology.
theorem
LinearMap.continuous_iInf'
{E : Type u_4}
{F : Type u_5}
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[CompleteSpace 𝕜]
[AddCommGroup E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[T2Space E]
[Module 𝕜 E]
[ContinuousSMul 𝕜 E]
[FiniteDimensional 𝕜 E]
[PseudoMetricSpace F]
[ProperSpace F]
[AddCommGroup F]
[IsTopologicalAddGroup F]
[T2Space F]
[Module 𝕜 F]
[ContinuousSMul 𝕜 F]
[FiniteDimensional 𝕜 F]
(f : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
{S : Set F}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨅ (y : ↑S), (f x) ↑y
A specialization of LinearMap.continuous_iInf to finite dimensional spaces, in place
of requiring a (non-instance) IsModuleTopology.
theorem
LinearMap.BilinForm.continuous_iSup
{𝕜 : Type u_4}
{E : Type u_5}
[RCLike 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
[ProperSpace E]
(f : LinearMap.BilinForm 𝕜 E)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨆ (y : ↑S), (f x) ↑y
Alias of LinearMap.continuous_iSup' that takes LinearMap.BilinForm.
theorem
LinearMap.BilinForm.continuous_iInf
{𝕜 : Type u_4}
{E : Type u_5}
[RCLike 𝕜]
[ConditionallyCompleteLinearOrder 𝕜]
[OrderTopology 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
[ProperSpace E]
(f : LinearMap.BilinForm 𝕜 E)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨅ (y : ↑S), (f x) ↑y
Alias of LinearMap.continuous_iInf' that takes LinearMap.BilinForm.
theorem
ContinuousLinearMap.continuous_iSup
{𝕜 : Type u_4}
{𝕜₂ : Type u_5}
{E : Type u_6}
{F : Type u_7}
{G : Type u_8}
[NontriviallyNormedField 𝕜]
[Semiring 𝕜₂]
{σ₁₂ : 𝕜₂ →+* 𝕜}
[SeminormedAddCommGroup E]
[NormedSpace 𝕜 E]
[ProperSpace E]
[AddCommMonoid F]
[TopologicalSpace F]
[Module 𝕜₂ F]
[SeminormedAddCommGroup G]
[NormedSpace 𝕜 G]
[ConditionallyCompleteLinearOrder G]
[OrderTopology G]
(f : F →SL[σ₁₂] E →L[𝕜] G)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : F) => ⨆ (y : ↑S), (f x) ↑y
A specialization of Bornology.IsBounded.continuous_iSup_bilinear to ContinuousLinearMap.
theorem
ContinuousLinearMap.continuous_iInf
{𝕜 : Type u_4}
{𝕜₂ : Type u_5}
{E : Type u_6}
{F : Type u_7}
{G : Type u_8}
[NontriviallyNormedField 𝕜]
[Semiring 𝕜₂]
{σ₁₂ : 𝕜₂ →+* 𝕜}
[SeminormedAddCommGroup E]
[NormedSpace 𝕜 E]
[ProperSpace E]
[AddCommMonoid F]
[TopologicalSpace F]
[Module 𝕜₂ F]
[SeminormedAddCommGroup G]
[NormedSpace 𝕜 G]
[ConditionallyCompleteLinearOrder G]
[OrderTopology G]
(f : F →SL[σ₁₂] E →L[𝕜] G)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : F) => ⨅ (y : ↑S), (f x) ↑y
theorem
LinearMap.BilinForm.continuous_iSup_fst
{E : Type u_4}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
(f : LinearMap.BilinForm ℝ E)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨆ (y : ↑S), (f ↑y) x
theorem
LinearMap.BilinForm.continuous_iInf_fst
{E : Type u_4}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
(f : LinearMap.BilinForm ℝ E)
{S : Set E}
(hS : Bornology.IsBounded S)
:
Continuous fun (x : E) => ⨅ (y : ↑S), (f ↑y) x