English
For any map T : X → X, set F ⊆ X, relation U ⊆ X × X, and n ∈ ℕ, the quantity coverMincard T F U n is finite (i.e., strictly less than the top element) if and only if there exists a finite subset s ⊆ X that forms a dynamical cover of T with respect to F and U at level n, and moreover s has cardinal equal to coverMincard T F U n.
Русский
Для отображения T : X → X, множества F ⊆ X, отношения U ⊆ X × X и натурального n, величина coverMincard T F U n конечна тогда и только тогда, когда существует конечная подмножество s ⊆ X, образующее динамическое покрытие T относительно F и U на уровне n, и при этом |s| = coverMincard T F U n.
LaTeX
$$$coverMincard(T,F,U,n) < \top \iff \exists s:\mathrm{Finset}(X),\ IsDynCoverOf(T,F,U,n,s) \wedge s.card = coverMincard(T,F,U,n)$$$
Lean4
theorem coverMincard_finite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
coverMincard T F U n < ⊤ ↔ ∃ s : Finset X, IsDynCoverOf T F U n s ∧ s.card = coverMincard T F U n :=
by
refine ⟨fun h_fin ↦ ?_, fun ⟨s, _, s_coverMincard⟩ ↦ s_coverMincard ▸ WithTop.coe_lt_top s.card⟩
obtain ⟨k, k_min⟩ := WithTop.ne_top_iff_exists.1 h_fin.ne
rw [← k_min]
simp only [ENat.some_eq_coe, Nat.cast_inj]
have : Nonempty { s : Finset X // IsDynCoverOf T F U n s } :=
by
by_contra h
apply ENat.coe_ne_top k
rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]
simp only [ENat.coe_ne_top, imp_false]
rw [nonempty_subtype, not_exists] at h
exact h
have key := ciInf_mem fun s : { s : Finset X // IsDynCoverOf T F U n s } ↦ (s.val.card : ℕ∞)
rw [coverMincard, iInf_subtype'] at k_min
rw [← k_min, mem_range, Subtype.exists] at key
simp only [ENat.some_eq_coe, Nat.cast_inj, exists_prop] at key
exact key
