cfcₙ_nonneg — Mathlib

English

For ha, hs with σ_n R a ⊆ s, cfc_nHomSuperset ha hs applied to the identity on s returns a.

Русский

Для ha, hs с σ_n R a ⊆ s отображение cfc_nHomSuperset ha hs(id_s) возвращает a.

LaTeX

$$$$ cfc\\!_nHomSuperset ha hs(\\mathrm{id}_s) = a $$$$

Lean4

theorem cfcₙ_nonneg {f : R → R} {a : A} (h : ∀ x ∈ σₙ R a, 0 ≤ f x) : 0 ≤ cfcₙ f a :=
  by
  by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
  · obtain ⟨h₁, h₂⟩ := hf
    simpa using cfcₙ_mono h
  · simp only [not_and_or] at hf
    obtain (hf | hf) := hf
    · simp only [cfcₙ_apply_of_not_continuousOn _ hf, le_rfl]
    · simp only [cfcₙ_apply_of_not_map_zero _ hf, le_rfl]

Похожие утверждения