of_comp_iff — Mathlib

English

The embedding status of a composition is determined by the embedding status of the inner map when the outer map is embedding.

Русский

Статус вложения композиции определяется вложенностью внутренней мапы при условии, что внешняя мапа вложение.

LaTeX

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

Lean4

theorem of_comp_iff {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} :
    IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f := by
  simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]

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