English
An antitone function sending bottom to top and continuous at the supremum of a set sends this supremum to the infimum of the image of the set.
Русский
Антизотонная функция, отправляющая нижнюю грань в верхнюю и непрерывная в верхнем пределе множества, переводит этот предел в наименьшее значение образа множества.
LaTeX
$$$Cf : ContinuousWithinAt f s (sSup s) \land Af : AntitoneOn f s \land f(\bot)=\top \Rightarrow f(sSup s) = sInf(f''s)$$$
Lean4
/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set. -/
theorem map_sSup_of_continuousWithinAt {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s))
(Af : AntitoneOn f s) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s) :=
MonotoneOn.map_sSup_of_continuousWithinAt (show ContinuousWithinAt (OrderDual.toDual ∘ f) s (sSup s) from Cf) Af fbot
