autEmbedding_range_isClosed — Mathlib

English

The embedding Aut F is a closed embedding.

Русский

Встраивание Aut F является замкнутым вложением.

LaTeX

$$IsClosedEmbedding(autEmbedding(F))$$

Lean4

/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` is closed. -/
theorem autEmbedding_range_isClosed : IsClosed (Set.range (autEmbedding F)) :=
  by
  rw [autEmbedding_range]
  refine isClosed_iInter (fun f ↦ isClosed_eq (X := F.obj f.left → F.obj f.right) ?_ ?_)
  · fun_prop
  · fun_prop

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