theorem Set.Finite.subset_sUnion_directedOn_iff {α : Type u_1} {s : Set α} (hs : s.Finite) {C : Set (Set α)} (hC : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) C) (hne : C.Nonempty) : s ⊆ ⋃₀ C ↔ ∃ t ∈ C, s ⊆ t

theorem Set.Finite.subset_biUnion_mono_iff {α : Type u_1} {s : Set α} {ι : Type u_2} [LE ι] {v : ι → Set α} {a : Set ι} (hs : s.Finite) (ha : DirectedOn (fun (x1 x2 : ι) => x1 ≤ x2) a) (hne : a.Nonempty) (hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j) : s ⊆ ⋃ i ∈ a, v i ↔ ∃ i ∈ a, s ⊆ v i

theorem Set.Finite.subset_iUnion_mono_iff {α : Type u_1} {s : Set α} {ι : Type u_2} [LE ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {v : ι → Set α} (hs : s.Finite) (hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j) : s ⊆ ⋃ (i : ι), v i ↔ ∃ (i : ι), s ⊆ v i

If s is an indexed directed family of sets, then a finite subset of their union is a subset of a set in the family.

@[simp]

theorem insert_infinite_iff {α : Type u_1} {x : α} {s : Set α} : (insert x s).Infinite ↔ s.Infinite

theorem Directed.iInter_mem_of_finite_mem {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (hdir : Directed (fun (x y : Set α) => y ⊆ x) s) (i₀ : ι) (hi : (s i₀).Finite) : ∃ (j : ι), s j = ⋂ (i : ι), s i

Every directed family of sets containing a finite set contains its intersection.

theorem DirectedOn.sInter_mem_of_finite_mem {α : Type u_1} (s : Set (Set α)) (hdir : DirectedOn (fun (x y : Set α) => y ⊆ x) s) {x : Set α} (hx : x ∈ s) (hfin : x.Finite) : ⋂₀ s ∈ s

theorem Directed.exists_forall_ge {α : Type u_2} {ι : Type u_3} [Preorder α] [Nonempty ι] {f : ι → α} (hdir : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) {I : Set ι} (hI : I.Finite) : ∃ (k : ι), ∀ i ∈ I, f i ≤ f k

theorem DirectedOn.exists_forall_ge {α : Type u_2} [Preorder α] {s t : Set α} (hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hne : s.Nonempty) (hts : t ⊆ s) (hfin : t.Finite) : ∃ x ∈ s, ∀ y ∈ t, y ≤ x

theorem DirectedOn.exists_forall_le {α : Type u_2} [Preorder α] {s t : Set α} (hdir : DirectedOn (fun (a b : α) => b ≤ a) s) (hne : s.Nonempty) (hts : t ⊆ s) (hfin : t.Finite) : ∃ x ∈ s, ∀ y ∈ t, x ≤ y

theorem Directed.exists_eq_iSup {α : Type u_2} {ι : Type u_3} [CompleteLattice α] [Finite ι] [Nonempty ι] {f : ι → α} (hdir : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) : ∃ (k : ι), f k = ⨆ (i : ι), f i

theorem DirectedOn.iSup_mem {α : Type u_2} [CompleteLattice α] {s : Set α} (hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hs : s.Nonempty) (hfin : s.Finite) : sSup s ∈ s

theorem Directed.exists_eq_iInf {α : Type u_2} {ι : Type u_3} [CompleteLattice α] [Finite ι] [Nonempty ι] {f : ι → α} (hdir : Directed (fun (a b : α) => b ≤ a) f) : ∃ (k : ι), f k = ⨅ (i : ι), f i

theorem DirectedOn.iInf_mem {α : Type u_2} [CompleteLattice α] {s : Set α} (hdir : DirectedOn (fun (a b : α) => b ≤ a) s) (hs : s.Nonempty) (hfin : s.Finite) : sInf s ∈ s