topologically_iso_le — Mathlib

English

If P holds for all homeomorphisms, then every scheme isomorphism induces a topologically P property.

Русский

Если свойство P выполняется для всех гомеоморфизмов, то изоморфизм схем порождает топологическое свойство P.

LaTeX

$$topologically P respects Iso$$

Lean4

/-- If a property of maps of topological spaces is satisfied by all homeomorphisms,
every isomorphism of schemes satisfies the induced property. -/
theorem topologically_iso_le (hP : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β), P f) :
    MorphismProperty.isomorphisms Scheme ≤ (topologically P) :=
  by
  intro X Y e (he : IsIso e)
  have : IsIso e := he
  exact hP (TopCat.homeoOfIso (asIso e.base))

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