continuousOn_sub — Mathlib

English

For ENNReal, the function p ↦ instHSub.hSub p.fst p.snd is continuous on the set of pairs (p) with p ≠ (∞, ∞).

Русский

Для ENNReal функция p ↦ p.fst − p.snd непрерывна на множестве пар с p ≠ (∞, ∞).

LaTeX

$$$\\\\text{ContinuousOn } (\\\\lambda p: p.fst - p.snd) \\\\{p: ENNReal \\times ENNReal \\\\mid p \neq (\\\\infty, \\\\infty)\\\\}. $$$

Lean4

theorem continuousOn_sub : ContinuousOn (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ ⟨∞, ∞⟩} :=
  by
  rw [ContinuousOn]
  rintro ⟨x, y⟩ hp
  simp only [Ne, Set.mem_setOf_eq, Prod.mk_inj] at hp
  exact tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

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