English
There exists a nonempty Finset t such that IsDynCoverOf holds for t and every x ∈ t intersects F in a nonempty ball.
Русский
Существует непустое конечное множество t, для которого выполняется покрытие и ∀ x ∈ t, (ball x ∩ F) непусто.
LaTeX
$$∃ t, IsDynCoverOf T F U n t ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F) ≠ ∅$$
Lean4
theorem nonempty_inter {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X} (h : IsDynCoverOf T F U n s) :
∃ t : Finset X, IsDynCoverOf T F U n t ∧ t.card ≤ s.card ∧ ∀ x ∈ t, ((ball x (dynEntourage T U n)) ∩ F).Nonempty :=
by
classical
use Finset.filter (fun x : X ↦ ((ball x (dynEntourage T U n)) ∩ F).Nonempty) s
simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]
refine ⟨fun y y_F ↦ ?_, Finset.card_mono (s.filter_subset _)⟩
specialize h y_F
simp only [mem_iUnion, exists_prop] at h
obtain ⟨z, z_s, y_Bz⟩ := h
simp only [mem_setOf_eq, mem_iUnion, exists_prop]
exact ⟨z, ⟨z_s, nonempty_of_mem ⟨y_Bz, y_F⟩⟩, y_Bz⟩
