English
Let X be a uniform space and T: X → X continuous. For any subset F ⊆ X, any U ⊆ X × X, and any V with V ∈ 𝓤(X), for every n ∈ ℕ we have coverMincard(T, closure(F), U ∘ V, n) ≤ coverMincard(T, F, U, n).
Русский
Пусть X — равномерное пространство, T: X → X непрерывно. Для любой подмножества F ⊆ X, любой U ⊆ X × X и любого V, удовлетворяющего V ∈ 𝓤(X), для всякого n ∈ ℕ выполнено: coverMincard(T, closure(F), U ∘ V, n) ≤ coverMincard(T, F, U, n).
LaTeX
$$$\operatorname{coverMincard}(T, \overline{F}, U\circ V, n) \le \operatorname{coverMincard}(T, F, U, n)$$$
Lean4
theorem coverMincard_closure_le (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)} (V_uni : V ∈ 𝓤 X)
(n : ℕ) : coverMincard T (closure F) (U ○ V) n ≤ coverMincard T F U n :=
by
rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'
· exact h' ▸ le_top
obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 h'
exact s_coverMincard ▸ (s_cover.closure h V_uni).coverMincard_le_card
