English
If P respects isomorphisms, then topologically P also respects isomorphisms.
Русский
Если P сохраняет изоморфизмы, то и топологически P сохраняет изоморфизмы.
LaTeX
$$topologically_respectsIso(P)$$
Lean4
/-- If a property of maps of topological spaces is satisfied by homeomorphisms and is stable
under composition, the induced property on schemes respects isomorphisms. -/
theorem topologically_respectsIso (hP₁ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β), P f)
(hP₂ :
∀ {α β γ : Type u} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α → β) (g : β → γ)
(_ : P f) (_ : P g), P (g ∘ f)) :
(topologically P).RespectsIso :=
have : (topologically P).IsStableUnderComposition := topologically_isStableUnderComposition P hP₂
MorphismProperty.respectsIso_of_isStableUnderComposition (topologically_iso_le P hP₁)
