continuous_piecewise_of_specializes

English

If x specializes to y and f is continuous, then f(x) specializes to f(y).

Русский

Если x специализируется на y и отображение непрерывно, то f(x) специализируется на f(y).

LaTeX

$$$$ x \rightsquigarrow y \rightarrow \text{Continuous } f \rightarrow f(x) \rightsquigarrow f(y). $$$$

Lean4

theorem continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsOpen s) (hf : Continuous f)
    (hg : Continuous g) (hspec : ∀ x, f x ⤳ g x) : Continuous (s.piecewise f g) :=
  by
  have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
  rw [continuous_def]
  intro U hU
  rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
  exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Похожие утверждения