restrictPreimage — Mathlib

English

The restriction of a continuous map to the preimage of a set gives a continuous map between the preimage and the set.

Русский

Ограничение непрерывного отображения на предобраз множества даёт непрерывное отображение между предобразом и самим множеством.

LaTeX

$$$\mathrm{restrictPreimage}(f,s) : C(f^{-1}'s, s)$$$

Lean4

/-- The restriction of a continuous map to the preimage of a set. -/
@[simps]
def restrictPreimage (f : C(α, β)) (s : Set β) : C(f ⁻¹' s, s) :=
  ⟨s.restrictPreimage f, continuous_iff_continuousAt.mpr fun _ ↦ (map_continuousAt f _).restrictPreimage⟩

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