continuous_sub_left — Mathlib

English

For ENNReal, the map a ↦ a − x is continuous in a for fixed x with a ≠ ∞.

Русский

Для ENNReal, отображение a ↦ a − x непрерывно по a, когда a ≠ ∞.

LaTeX

$$$\\\\forall x, a \\\\neq ∞ \\\\Rightarrow \\\\text{Continuous at } a: (a \\mapsto a - x).$$$

Lean4

theorem continuous_sub_left {a : ℝ≥0∞} (a_ne_top : a ≠ ∞) : Continuous (a - ·) :=
  by
  change Continuous (Function.uncurry Sub.sub ∘ (a, ·))
  refine continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_
  simp only [a_ne_top, Ne, mem_setOf_eq, Prod.mk_inj, false_and, not_false_iff]

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