English
If f is a directed family of sets indexed by I, and s ⊆ ⋃_{i ∈ I} f(i) is a finite set, then there exists i ∈ I with s ⊆ f(i).
Русский
Если семейство множеств {f(i)} по индексам I направлено по включению и конечное подмножество s подпадает в объединение, то найдётся индекс i с s ⊆ f(i).
LaTeX
$$$\\text{Directed}(\\subseteq)\\ f\\ I,\\ hs: (s)\\subseteq \\bigcup_{i \\in I} f(i) \\Rightarrow \\exists i, s \\subseteq f(i)$$$
Lean4
theorem exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι] {f : ι → Set α} (h : Directed (· ⊆ ·) f)
{s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) : ∃ i, (s : Set α) ⊆ f i := by
induction s using Finset.cons_induction with
| empty => simp
| cons b t hbt iht =>
simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
rcases h i j with ⟨k, hik, hjk⟩
exact ⟨k, hik hi, hj.trans hjk⟩
