English
If s is open, then ContinuousOn f s is equivalent to a family of open approximations via intersections with preimages of open sets.
Русский
Если s открыто, то ContinuousOn f s эквивалентно семейству открытых аппроксимаций через пересечения с предобразами открытых множеств.
LaTeX
$$$\\text{IsOpen}(s) \\Rightarrow \\text{ContinuousOn } f s \\iff \\forall t, IsOpen(t) \\rightarrow IsOpen(s \\cap f^{-1}(t))$$$
Lean4
theorem continuousOn_open_iff (hs : IsOpen s) : ContinuousOn f s ↔ ∀ t, IsOpen t → IsOpen (s ∩ f ⁻¹' t) :=
by
rw [continuousOn_iff']
constructor
· intro h t ht
rcases h t ht with ⟨u, u_open, hu⟩
rw [inter_comm, hu]
apply IsOpen.inter u_open hs
· intro h t ht
refine ⟨s ∩ f ⁻¹' t, h t ht, ?_⟩
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]
