English
For functions f mapping α into a linear order γ with OrderTopology, continuity within a set s at x is equivalent to the conjunction of lower and upper semicontinuity within s at x.
Русский
Для функций f: α → γ, непрерывность внутри на s в x эквивалентна союзу нижней и верхней полупрерывности внутри s на x.
LaTeX
$$$$\\operatorname{ContinuousWithinAt} f\_s x \\iff \\operatorname{LowerSemicontinuousWithinAt} f\_s x \\land \\operatorname{UpperSemicontinuousWithinAt} f\_s x.$$$$
Lean4
theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt {f : α → γ} :
ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x :=
by
refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩
rintro ⟨h₁, h₂⟩
intro v hv
simp only [Filter.mem_map]
by_cases Hl : ∃ l, l < f x
· rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
by_cases Hu : ∃ u, f x < u
· rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
rcases le_or_gt (f a) (f x) with h | h
· exact hl ⟨lfa, h⟩
· exact hu ⟨le_of_lt h, fau⟩
· simp only [not_exists, not_lt] at Hu
filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩
· simp only [not_exists, not_lt] at Hl
by_cases Hu : ∃ u, f x < u
· rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
filter_upwards [h₂ u fxu] with a lfa
apply hu
exact ⟨Hl (f a), lfa⟩
· simp only [not_exists, not_lt] at Hu
apply Filter.Eventually.of_forall
intro a
have : f a = f x := le_antisymm (Hu _) (Hl _)
rw [this]
exact mem_of_mem_nhds hv
