Set unions, intersections, and order

This file contains results connecting indexed unions and intersections of sets with order structures. It covers intersections of intervals, tails of families indexed by natural numbers, and the interaction of set unions with complete-lattice suprema and infima.

Intervals

theorem Set.nonempty_iInter_Iic_iff {α : Type u_1} {ι : Sort u_3} [Preorder α] {f : ι → α} : (⋂ (i : ι), Iic (f i)).Nonempty ↔ BddBelow (range f)

theorem Set.nonempty_iInter_Ici_iff {α : Type u_1} {ι : Sort u_3} [Preorder α] {f : ι → α} : (⋂ (i : ι), Ici (f i)).Nonempty ↔ BddAbove (range f)

theorem Set.Ici_iSup {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ι → α) : Ici (⨆ (i : ι), f i) = ⋂ (i : ι), Ici (f i)

theorem Set.Iic_iInf {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ι → α) : Iic (⨅ (i : ι), f i) = ⋂ (i : ι), Iic (f i)

theorem Set.Ici_iSup₂ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [CompleteLattice α] (f : (i : ι) → κ i → α) : Ici (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), Ici (f i j)

theorem Set.Iic_iInf₂ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [CompleteLattice α] (f : (i : ι) → κ i → α) : Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), Iic (f i j)

theorem Set.Ici_sSup {α : Type u_1} [CompleteLattice α] (s : Set α) : Ici (sSup s) = ⋂ a ∈ s, Ici a

theorem Set.Iic_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) : Iic (sInf s) = ⋂ a ∈ s, Iic a

theorem Set.iUnion_ge_eq_iUnion_nat_add {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : ⋃ (i : ℕ), ⋃ (_ : i ≥ n), u i = ⋃ (i : ℕ), u (i + n)

theorem Set.iInter_ge_eq_iInter_nat_add {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : ⋂ (i : ℕ), ⋂ (_ : i ≥ n), u i = ⋂ (i : ℕ), u (i + n)

theorem Monotone.iUnion_nat_add {α : Type u_1} {f : ℕ → Set α} (hf : Monotone f) (k : ℕ) : ⋃ (n : ℕ), f (n + k) = ⋃ (n : ℕ), f n

theorem Antitone.iInter_nat_add {α : Type u_1} {f : ℕ → Set α} (hf : Antitone f) (k : ℕ) : ⋂ (n : ℕ), f (n + k) = ⋂ (n : ℕ), f n

@[simp]

theorem Set.iUnion_iInter_ge_nat_add {α : Type u_1} (f : ℕ → Set α) (k : ℕ) : ⋃ (n : ℕ), ⋂ (i : ℕ), ⋂ (_ : i ≥ n), f (i + k) = ⋃ (n : ℕ), ⋂ (i : ℕ), ⋂ (_ : i ≥ n), f i

theorem Set.union_iUnion_nat_succ {α : Type u_1} (u : ℕ → Set α) : u 0 ∪ ⋃ (i : ℕ), u (i + 1) = ⋃ (i : ℕ), u i

theorem Set.inter_iInter_nat_succ {α : Type u_1} (u : ℕ → Set α) : u 0 ∩ ⋂ (i : ℕ), u (i + 1) = ⋂ (i : ℕ), u i

theorem Set.iUnion_le_nat : ⋃ (n : ℕ), {i : ℕ | i ≤ n} = univ

theorem iSup_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨆ a ∈ ⋃ (i : ι), s i, f a = ⨆ (i : ι), ⨆ a ∈ s i, f a

theorem iInf_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨅ a ∈ ⋃ (i : ι), s i, f a = ⨅ (i : ι), ⨅ a ∈ s i, f a

theorem sSup_iUnion {β : Type u_2} {ι : Sort u_3} [CompleteLattice β] (t : ι → Set β) : sSup (⋃ (i : ι), t i) = ⨆ (i : ι), sSup (t i)

theorem sSup_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) : sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

theorem sInf_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) : sInf (⋃₀ s) = ⨅ t ∈ s, sInf t

theorem iSup_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) : ⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

theorem iInf_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) : ⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

theorem forall_sUnion {α : Type u_1} {S : Set (Set α)} {p : α → Prop} : (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

theorem exists_sUnion {α : Type u_1} {S : Set (Set α)} {p : α → Prop} : (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x