cover with property

Stream: maths

[Johan Commelin]

In the definition of adic_space we have:

(Hlocally_affinoid : ∃ (I : Type u) (U : I → opens X) (Hcover : set.Union (λ i, (U i).1) = set.univ)
  (R : I → Huber_pair.{u}),
  ∀ i : I, nonempty (𝒞.equiv (𝒞.Spa (R i)) (𝒞.restrict (U i) locally_ringed_valued_space.to_𝒞)))

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/adic_space.lean#L402
On the other hand, in the definition of perfectoid_space we have

(perfectoid_cover : ∀ x : X, ∃ (U : opens X) (A : Huber_pair) [perfectoid_ring A],
(x ∈ U) ∧ (𝒞.Spa A) ≅_𝒞 (locally_ringed_valued_space.to_𝒞.restrict U))

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/perfectoid_space.lean#L28

Both express the condition that there exists a cover of the space by open subsets satisfying some condition. However, they are phrased a bit differently. Are there reasons to prefer one over the other? Does mathlib already have some sort of preference/standard here?

[Kevin Buzzard]

To clarify a bit: I guess we want to say, on two occasions, that our topological space $X$ is covered by open sets each of which has a nice property; the first time we say "there's a random type $I$ and a map from $I$ to the set of open subsets of $X$ such that the union of the image sets is $X$"; the second time we say $\forall x\in X\, \exists U\subseteq X$ open with $x\in U$ and $U$ nice.