universallyClosed_respectsIso — Mathlib

English

UniversallyClosed respects isomorphisms: the property is invariant under isomorphisms of schemes.

Русский

UniversallyClosed сохраняется при изоморфизмах схем: свойство не меняется под изоморфизмами.

LaTeX

$$$\\mathrm{RespectsIso}(\\mathrm{UniversallyClosed})$$$

Lean4

theorem universallyClosed_respectsIso : RespectsIso @UniversallyClosed :=
  universallyClosed_eq.symm ▸ universally_respectsIso (topologically @IsClosedMap)

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