comp — Mathlib

English

If g is a uniform embedding and f is a uniform embedding, then the composition g ∘ f is a uniform embedding.

Русский

Если $g$ и $f$ — равномерные вложения, то композиция $g\\circ f$ тоже является равномерным вложением.

LaTeX

$$$\\displaystyle \\text{IsUniformEmbedding}(g\\circ f) \\iff \\text{IsUniformEmbedding}(f)\\text{ when } \\text{IsUniformEmbedding}(g)$$$

Lean4

theorem comp {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} (hf : IsUniformEmbedding f) :
    IsUniformEmbedding (g ∘ f)
    where
  toIsUniformInducing := hg.isUniformInducing.comp hf.isUniformInducing
  injective := hg.injective.comp hf.injective

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