Continuity of finite indexed suprema and infima #
In a conditionally complete lattice with continuous binary suprema, the pointwise supremum
x ↦ ⨆ i, f i x of a finite family of continuous functions is continuous, and dually for
infima. An empty family has the constant supremum sSup ∅. These are the indexed-supremum
forms of Mathlib's Continuous.finset_sup'_apply and Continuous.finset_inf'_apply, convenient
when the supremum is written with ⨆ over a finite type, such as a Finset coerced to a type.
theorem
TauCeti.continuous_ciSup_of_finite
{X : Type u_1}
{L : Type u_2}
{ι : Type u_3}
[TopologicalSpace X]
[ConditionallyCompleteLattice L]
[TopologicalSpace L]
[Finite ι]
[ContinuousSup L]
{f : ι → X → L}
(hf : ∀ (i : ι), Continuous (f i))
:
Continuous fun (x : X) => ⨆ (i : ι), f i x
The pointwise supremum of a finite family of continuous functions is continuous.
theorem
TauCeti.continuous_ciInf_of_finite
{X : Type u_1}
{L : Type u_2}
{ι : Type u_3}
[TopologicalSpace X]
[ConditionallyCompleteLattice L]
[TopologicalSpace L]
[Finite ι]
[ContinuousInf L]
{f : ι → X → L}
(hf : ∀ (i : ι), Continuous (f i))
:
Continuous fun (x : X) => ⨅ (i : ι), f i x
The pointwise infimum of a finite family of continuous functions is continuous.