continuous_sub_right — Mathlib

English

For ENNReal, the map x ↦ x − a is continuous for all a, with the special case when a = ∞ handled separately.

Русский

Для ENNReal отображение x ↦ x − a непрерывно при любом a; случай a = ∞ обсуждается отдельно.

LaTeX

$$$\\\\forall a, \\\\text{Continuous } (\\\\lambda x: x - a).$$$

Lean4

theorem continuous_sub_right (a : ℝ≥0∞) : Continuous fun x : ℝ≥0∞ => x - a :=
  by
  by_cases a_infty : a = ∞
  · simp [a_infty, continuous_const, tsub_eq_zero_of_le]
  · rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
    apply continuousOn_sub.comp_continuous (by fun_prop)
    intro x
    simp only [a_infty, Ne, mem_setOf_eq, Prod.mk_inj, and_false, not_false_iff]

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