theorem ContinuousFunctions.continuous_iff_isOpen_preimage {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : [Continuous f, ∀ (O : Set Y), IsOpen O → IsOpen (f ⁻¹' O), ∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C), SeqContinuous f].TFAE

For maps between metric spaces, the following are equivalent: continuity, openness of preimages of open sets, closedness of preimages of closed sets, and sequential continuity (Melrose Prop 1.1).

noncomputable def ContinuousFunctions.zeroAtInftyPosPart {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) : ZeroAtInftyContinuousMap X ℝ

Positive part f⁺ = max(f, 0) of a real-valued continuous function vanishing at infinity, itself in C₀(X, ℝ).

noncomputable def ContinuousFunctions.zeroAtInftyNegPart {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) : ZeroAtInftyContinuousMap X ℝ

Negative part f⁻ = max(-f, 0) of a real-valued continuous function vanishing at infinity, itself in C₀(X, ℝ).

@[simp]

theorem ContinuousFunctions.posPart_apply {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : (zeroAtInftyPosPart f) x = max (f x) 0

Pointwise evaluation of the positive part: f⁺(x) = max(f(x), 0).

@[simp]

theorem ContinuousFunctions.negPart_apply {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : (zeroAtInftyNegPart f) x = max (-f x) 0

Pointwise evaluation of the negative part: f⁻(x) = max(-f(x), 0).

theorem ContinuousFunctions.decompose_pos_neg {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) : f = zeroAtInftyPosPart f - zeroAtInftyNegPart f

Decomposition f = f⁺ - f⁻ in C₀(X, ℝ).

theorem ContinuousFunctions.posPart_le_abs {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : (zeroAtInftyPosPart f) x ≤ |f x|

Pointwise bound: f⁺(x) ≤ |f(x)|.

theorem ContinuousFunctions.negPart_le_abs {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : (zeroAtInftyNegPart f) x ≤ |f x|

Pointwise bound: f⁻(x) ≤ |f(x)|.

theorem ContinuousFunctions.posPart_nonneg {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : 0 ≤ (zeroAtInftyPosPart f) x

Nonnegativity of the positive part: 0 ≤ f⁺(x).

theorem ContinuousFunctions.negPart_nonneg {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) (x : X) : 0 ≤ (zeroAtInftyNegPart f) x

Nonnegativity of the negative part: 0 ≤ f⁻(x).

theorem ContinuousFunctions.decompose_unique {X : Type u_1} [TopologicalSpace X] (f g h : ZeroAtInftyContinuousMap X ℝ) (hdecomp : f = g - h) (hg_nonneg : ∀ (x : X), 0 ≤ g x) (hh_nonneg : ∀ (x : X), 0 ≤ h x) (hg_le : ∀ (x : X), g x ≤ |f x|) (hh_le : ∀ (x : X), h x ≤ |f x|) : g = zeroAtInftyPosPart f ∧ h = zeroAtInftyNegPart f

Uniqueness of the f⁺/f⁻ decomposition: any decomposition f = g - h with g, h both nonnegative and pointwise bounded by |f| must coincide with (f⁺, f⁻).

theorem ContinuousFunctions.zeroAtInfty_unique_posNeg_decomposition {X : Type u_1} [TopologicalSpace X] (f : ZeroAtInftyContinuousMap X ℝ) : f = zeroAtInftyPosPart f - zeroAtInftyNegPart f ∧ (∀ (x : X), (zeroAtInftyPosPart f) x ≤ |f x|) ∧ (∀ (x : X), (zeroAtInftyNegPart f) x ≤ |f x|) ∧ ∀ (g h : ZeroAtInftyContinuousMap X ℝ), f = g - h → (∀ (x : X), 0 ≤ g x) → (∀ (x : X), 0 ≤ h x) → (∀ (x : X), g x ≤ |f x|) → (∀ (x : X), h x ≤ |f x|) → g = zeroAtInftyPosPart f ∧ h = zeroAtInftyNegPart f

Combined statement (Melrose Lemma 1.4): every f ∈ C₀(X, ℝ) admits the canonical positive/negative decomposition f = f⁺ - f⁻ with the appropriate dominance bounds, and the decomposition is unique among such pairs.

def NormedSpaces.AreEquivalentNorms {V : Type u_1} (norm₁ norm₂ : V → ℝ) : Prop

Two norms on V are equivalent if they are mutually controlled by a single positive constant, i.e. (1/C) · norm₁ v ≤ norm₂ v ≤ C · norm₁ v for all v.

theorem NormedSpaces.finDim_norms_equivalent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃ₗ[𝕜] F) : AreEquivalentNorms (fun (v : E) => ‖v‖) fun (v : E) => ‖e v‖

Equivalence of norms on finite-dimensional vector spaces: any linear isomorphism between finite-dimensional normed spaces gives rise to equivalent norms v ↦ ‖v‖ and v ↦ ‖e v‖.

theorem ContinuousLinearFunctional.continuousAt_zero_of_continuous {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : V →ₗ[ℝ] ℝ) (h : Continuous ⇑u) : ContinuousAt (⇑u) 0

A continuous linear functional is continuous at the origin.

theorem ContinuousLinearFunctional.bounded_image_closedBall_of_continuousAt_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : V →ₗ[ℝ] ℝ) (h : ContinuousAt (⇑u) 0) : Bornology.IsBounded (⇑u '' {f : V | ‖f‖ ≤ 1})

A linear functional continuous at the origin sends the closed unit ball to a bounded set.

theorem ContinuousLinearFunctional.bound_of_bounded_image_closedBall {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : V →ₗ[ℝ] ℝ) (h : Bornology.IsBounded (⇑u '' {f : V | ‖f‖ ≤ 1})) : ∃ (C : ℝ), ∀ (f : V), ‖u f‖ ≤ C * ‖f‖

If a linear functional sends the unit ball to a bounded set, it satisfies a global linear bound ‖u f‖ ≤ C · ‖f‖.

theorem ContinuousLinearFunctional.continuous_of_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : V →ₗ[ℝ] ℝ) (h : ∃ (C : ℝ), ∀ (f : V), ‖u f‖ ≤ C * ‖f‖) : Continuous ⇑u

A linear functional satisfying a global linear bound ‖u f‖ ≤ C · ‖f‖ is continuous.

theorem ContinuousLinearFunctional.linearFunctional_continuous_tfae {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : V →ₗ[ℝ] ℝ) : [Continuous ⇑u, ContinuousAt (⇑u) 0, Bornology.IsBounded (⇑u '' {f : V | ‖f‖ ≤ 1}), ∃ (C : ℝ), ∀ (f : V), ‖u f‖ ≤ C * ‖f‖].TFAE

The four standard characterisations of continuity for a real linear functional on a real normed space are equivalent: global continuity, continuity at zero, bounded image of the unit ball, and existence of an operator-norm bound.