lowerSemicontinuous_add — Mathlib

English

The map (p1,p2) ↦ p1+p2 from EReal × EReal to EReal is lower semicontinuous.

Русский

Отображение (p1,p2) ↦ p1+p2 с EReal × EReal в EReal является нижне полусцепной непрерывностью.

LaTeX

$$$\\mathrm{LowerSemicontinuous}\\bigl((p_1,p_2) \\mapsto p_1+p_2\\bigr)$$$

Lean4

theorem lowerSemicontinuous_add : LowerSemicontinuous fun p : EReal × EReal ↦ p.1 + p.2 :=
  by
  intro x y
  by_cases hx₁ : x.1 = ⊥
  · simp [hx₁]
  by_cases hx₂ : x.2 = ⊥
  · simp [hx₂]
  · exact continuousAt_add (.inr hx₂) (.inl hx₁) |>.lowerSemicontinuousAt _

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