English
ContinuousOn f s is equivalent to the property that for every t closed in β, there exists a closed u in α such that f^{-1}(t) ∩ s = u ∩ s.
Русский
ContinuousOn f s эквивалентна тому, что для каждого замкнутого t в β существует замкнутое u в α с f^{-1}(t) ∩ s = u ∩ s.
LaTeX
$$$\\text{ContinuousOn } f s \\iff ∀ t, IsClosed t \\to \\exists u, IsClosed u ∧ f^{-1}(t) ∩ s = u ∩ s$$$
Lean4
theorem continuousOn_iff_isClosed :
ContinuousOn f s ↔ ∀ t : Set β, IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
by
have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
by
intro t
rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]
rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]; simp only [this]
