eq_valuativeCriterion — Mathlib

English

Equality between two formulations of the valuative criterion: IsSeparated.valuativeCriterion ≡ ValuativeCriterion.Uniqueness ∧ QuasiSeparated.

Русский

Эквивалентность двух формулировок валюативного критерия: IsSeparated.valuativeCriterion эквивалентен ValuativeCriterion.Uniqueness ∧ QuasiSeparated.

LaTeX

$$IsSeparated.valuativeCriterion = ValuativeCriterion.Uniqueness ∧ QuasiSeparated$$

Lean4

/-- The **valuative criterion** for separated morphisms. -/
theorem eq_valuativeCriterion : @IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated :=
  by
  ext X Y f
  exact ⟨fun _ ↦ ⟨IsSeparated.valuativeCriterion f, inferInstance⟩, fun ⟨H, _⟩ ↦ .of_valuativeCriterion f H⟩

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