restrictPreimage_isEmbedding — Mathlib

English

If f is an embedding, then restricting its preimage to any set s is still an embedding.

Русский

Если f является внедрением, то ограничение прообраза на любой набор s тоже является внедрением.

LaTeX

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

Lean4

theorem restrictPreimage_isEmbedding (s : Set β) (h : IsEmbedding f) : IsEmbedding (s.restrictPreimage f) :=
  ⟨h.1.restrictPreimage s, h.2.restrictPreimage s⟩

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