continuousOn_sub_left — Mathlib

English

The map a − · is continuous on {x ≠ ∞} for any a ∈ ENNReal.

Русский

Отображение a − x непрерывно на множествах x ≠ ∞ для любого a ∈ ENNReal.

LaTeX

$$$\\\\forall a \\\\in ENNReal, \\\\text{ContinuousOn } (\\\\lambda x: a - x) \\\\{x \\neq \\infty\\}.$$$

Lean4

theorem continuousOn_sub_left (a : ℝ≥0∞) : ContinuousOn (a - ·) {x : ℝ≥0∞ | x ≠ ∞} :=
  by
  rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]
  apply continuousOn_sub.comp (by fun_prop)
  rintro _ h (_ | _)
  exact h none_eq_top

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