topologically — Mathlib

English

topologically P is the scheme morphism property obtained by evaluating the base map with P on the underlying space.

Русский

topologically P — это свойство морфизмов схем, получаемое путем применения P к базовой карте на основе.

LaTeX

$$topologically(P) := (fun _ _ f => P(f.base))$$

Lean4

/-- `topologically P` holds for a morphism if the underlying topological map satisfies `P`. -/
def topologically (P : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (_ : α → β), Prop) :
    MorphismProperty Scheme.{u} := fun _ _ f => P f.base

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