iff_of_iSup_eq_top — Mathlib

English

Let U : ι → X.Open, with iSup U = ⊤. Then P f is equivalent to P((U i).ι ≫ f) for all i; i.e., P is detected on an open cover of the source.

Русский

Пусть U : ι → X.Open и iSup U = ⊤. Тогда P f эквивалентно P((U i).ι ≫ f) для всех i; то есть свойство P определяется по открытому покрытию источника.

LaTeX

$$$\forall {U : ι \to X^{\mathrm{Opens}}} (hU : iSup U = \top),\\ P f \iff \forall i, P((U i).\iota ≫ f).$$$

Lean4

theorem iff_of_iSup_eq_top {ι} (U : ι → X.Opens) (hU : iSup U = ⊤) : P f ↔ ∀ i, P ((U i).ι ≫ f) :=
  ⟨fun H _ ↦ comp H _, of_iSup_eq_top U hU⟩

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