restrictPreimage_isInducing — Mathlib

English

If f is inducing, then restricting preimages to a set s preserves the inducing property.

Русский

Если f восстанавливает структуру непрерывности через подпространство, то ограничение на прообраз сохраняет это свойство.

LaTeX

$$$IsInducing f \\rightarrow IsInducing (s.restrictPreimage f)$$$

Lean4

theorem restrictPreimage_isInducing (s : Set β) (h : IsInducing f) : IsInducing (s.restrictPreimage f) :=
  by
  simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage, MapsTo.coe_restrict, restrict_eq,
    ← @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h ⊢
  intro a
  rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]

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