of_comp — Mathlib

English

If f and g are continuous and g ∘ f is an embedding, then f is an embedding.

Русский

Если f и g непрерывны и их композиция g ∘ f является вложением, то f является вложением.

LaTeX

$$$\text{Continuous}(f) \land \text{Continuous}(g) \land \mathrm{IsEmbedding}(g \circ f) \Rightarrow \mathrm{IsEmbedding}(f)$$$

Lean4

protected theorem of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsEmbedding (g ∘ f)) : IsEmbedding f
    where
  toIsInducing := hgf.isInducing.of_comp hf hg
  injective := hgf.injective.of_comp

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