English
ContinuousOn f s is equivalent to the continuity of f restricted via an open embedding, as captured by ContinuousOn_iff'.
Русский
ContinuousOn f s эквивалентна непрерывности ограниченного отображения через открытое вложение, выражаемое через ContinuousOn_iff'.
LaTeX
$$$\\text{ContinuousOn } f s \\iff \\forall t, IsOpen t \\to \\exists u, IsOpen u \\land f^{-1}(t)\\cap s = u\\cap s$$$
Lean4
theorem continuousOn_iff' : ContinuousOn f s ↔ ∀ t : Set β, IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
by
have : ∀ t, IsOpen (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
by
intro t
rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
constructor <;>
· rintro ⟨u, ou, useq⟩
exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩
rw [continuousOn_iff_continuous_restrict, continuous_def]; simp only [this]
