iUnion_range — Mathlib

English

For a jointly surjective cover 𝒰, the union of the ranges of opens equals the entire space.

Русский

Для jointly surjective покрытия 𝒰 объединение диапазонов открытий равно всей области пространства.

LaTeX

$$$$ \bigcup_i \operatorname{range}(\mathrm{opensRange}(\mathcal{U}.f i)) = \top $$$$

Lean4

theorem iUnion_range [JointlySurjective K] {X : Scheme.{u}} (𝒰 : X.Cover K) : ⋃ i, Set.range (𝒰.f i).base = Set.univ :=
  by
  rw [Set.eq_univ_iff_forall]
  intro x
  rw [Set.mem_iUnion]
  exact 𝒰.exists_eq x

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