English
Analogous equivalence for ConcaveOn: the same list of equivalent conditions after negation.
Русский
Аналогично для ConcaveOn: те же эквивалентные условия после отрицания.
LaTeX
$$“The same list of equivalences after negation”$$
Lean4
theorem continuousOn_tfae (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConcaveOn ℝ C f) :
TFAE
[LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀, ∃ x₀ ∈ C, (𝓝 x₀).IsBoundedUnder (· ≥ ·) f,
∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≥ ·) f, ∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f|] :=
by
have := hf.neg.continuousOn_tfae hC hC'
simp only [locallyLipschitzOn_neg_iff, continuousOn_neg_iff, continuousAt_neg_iff, abs_neg] at this
convert this using 8 <;> exact (Equiv.neg ℝ).exists_congr (by simp)
