exists_mem_subset_of_finset_subset_biUnion

English

Let c be a nonempty set of indices with f(i) ⊆ f(j) for i ≤ j, then any finite subset s of ⋃_{i∈c} f(i) is contained in some f(i) with i ∈ c.

Русский

Пусть c — непустое множество индексов, упорядованных включением, тогда любая конечная подмножество из объединения f(i) содержится в некотором f(i) с i ∈ c.

LaTeX

$$$\\exists i \\in c,\\ (s \\subseteq f(i))$ given nonempty c and directedOn containment$$

Lean4

theorem exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α} {c : Set ι} (hn : c.Nonempty)
    (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) :
    ∃ i ∈ c, (s : Set α) ⊆ f i := by
  rw [Set.biUnion_eq_iUnion] at hs
  haveI := hn.coe_sort
  simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Похожие утверждения