of_comp_iff — Mathlib

English

If g is a closed embedding, then IsClosedEmbedding (g ∘ f) iff IsClosedEmbedding f.

Русский

Если g — замкнутое вложение, то IsClosedEmbedding (g ∘ f) эквивалично IsClosedEmbedding f.

LaTeX

$$$\mathrm{IsClosedEmbedding}(g) \rightarrow (\mathrm{IsClosedEmbedding}(g \circ f) \leftrightarrow \mathrm{IsClosedEmbedding}(f))$$$

Lean4

theorem of_comp_iff (hg : IsClosedEmbedding g) : IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f := by
  simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp, ← hg.isClosed_iff_image_isClosed]

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