exists_mem_subset_of_finite_of_subset_sUnion

English

If c is nonempty and directedOn by ⊆, and s is finite with s ⊆ ⋃_{i∈c} f(i), then ∃ t ∈ c with s ⊆ f(t).

Русский

Если c непусто и направлено по ⊆, и конечное множество s ⊆ ⋃_{i∈c} f(i), то существует t ∈ c такое, что s ⊆ f(t).

LaTeX

$$$c\\neq \\emptyset \\land DirectedOn( (\\subseteq) ) c \\rightarrow ( s\\ finite \\land s \\subseteq \\bigcup_{i\\in c} f(i) ) \\rightarrow \\exists t\\in c,\\ s\\subseteq f(t)$$$

Lean4

theorem exists_mem_subset_of_finite_of_subset_sUnion {α : Type*} {c : Set (Set α)} (hn : c.Nonempty)
    (hc : DirectedOn (· ⊆ ·) c) {s : Set α} (hs : s.Finite) (hsc : s ⊆ sUnion c) : ∃ t ∈ c, s ⊆ t :=
  by
  rw [← hs.coe_toFinset, sUnion_eq_biUnion] at hsc
  have := DirectedOn.exists_mem_subset_of_finset_subset_biUnion hn hc hsc
  exact hs.coe_toFinset ▸ this

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