English
A set U is compact-open covered by a family of maps f_i from spaces X_i to S exactly when U can be expressed as a finite union of images f_i[V_i] where each V_i is an open subset of X_i and each V_i is mapped from a compact set.
Русский
Множество U покрывается компактно-открытым образом семейством отображений f_i: X_i → S тогда и только тогда, когда U может быть выражено как конечная объединение образов f_i[V_i], где каждый V_i — открытое подмножество X_i, и соответствующая часть V_i компактна.
LaTeX
$$$\mathrm{IsCompactOpenCovered}(f,U) \;\text{iff}\; \exists s \subseteq ι, s \text{ finite},\; \exists V_i \ (i ∈ s) \text{ с } V_i \in \mathrm{Opens}(X_i), \forall i∈s, \mathrm{IsCompact}(V_i), \; U = \bigcup_{i∈s} f(i)''V_i.$$$
Lean4
/-- A set `U` is compact-open covered by the family `fᵢ : X i → S`, if
`U` is the finite union of images of compact open sets in the `X i`. -/
def IsCompactOpenCovered {S ι : Type*} {X : ι → Type*} (f : ∀ i, X i → S) [∀ i, TopologicalSpace (X i)] (U : Set S) :
Prop :=
∃ (s : Set ι) (_ : s.Finite) (V : ∀ i ∈ s, Opens (X i)),
(∀ (i : ι) (h : i ∈ s), IsCompact (V i h).1) ∧ ⋃ (i : ι) (h : i ∈ s), (f i) '' (V i h) = U
