iff_of_openCover — Mathlib

English

Let 𝒰 be an open cover of X. Then P f holds iff P((𝒰.f i) ≫ f) holds for all i in 𝒰.

Русский

Пусть 𝒰 — открытое покрытие X. Тогда P f выполняется тогда и только тогда, когда P((𝒰.f i) ≫ f) выполняется для всех i из 𝒰.

LaTeX

$$$\forall {P : \mathrm{MorphismProperty}(\mathrm{Scheme})} [IsZariskiLocalAtSource P], (\forall i, P((\mathcal{U}.f i) ≫ f)) \iff P f.$$$

Lean4

theorem iff_of_openCover : P f ↔ ∀ i, P (𝒰.f i ≫ f) :=
  ⟨fun H _ ↦ comp H _, of_openCover _⟩

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