Indexed unions and intersections of sets

A set defined by a condition Φ on the tuple of values of a family of functions is the union, over the tuples satisfying Φ, of the fibres of the family over those tuples.

The union of the binary family ![U, V] is U ∪ V.

Main results

• Set.iUnion_vecCons_pair: the union of a family of two sets.
• TauCeti.setOf_apply_eq_biUnion_iInter: {x | Φ (g · x)} = ⋃ ε ∈ {ε | Φ ε}, ⋂ i, {x | g i x = ε i}.
• TauCeti.exists_notMem_succ_of_notMem_iInter: a point outside the intersection of a decreasing sequence of sets lies outside K (k + 1) for some k.
• TauCeti.exists_map_eq_of_notMem: a map taking the eventual value of maps which stabilize outside a decreasing sequence of sets, with a prescribed value on the intersection.

@[simp]

theorem Set.iUnion_vecCons_pair {X : Type u_1} (U V : Set X) : ⋃ (i : Fin (Nat.succ 0).succ), ![U, V] i = U ∪ V

The union of the binary family ![U, V] is U ∪ V.

theorem TauCeti.setOf_apply_eq_biUnion_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} (g : ι → α → β) (Φ : (ι → β) → Prop) : {x : α | Φ fun (i : ι) => g i x} = ⋃ ε ∈ {ε : ι → β | Φ ε}, ⋂ (i : ι), {x : α | g i x = ε i}

The set of points where a family of functions g i satisfies a condition Φ on its tuple of values is the union, over the tuples ε satisfying Φ, of the sets where g i = ε i for all i.

theorem TauCeti.exists_notMem_succ_of_notMem_iInter {α : Type u_1} {K : ℕ → Set α} (hKsucc : ∀ (i : ℕ), K (i + 1) ⊆ K i) {x : α} (hx : x ∉ ⋂ (i : ℕ), K i) : ∃ (k : ℕ), x ∉ K (k + 1)

A point outside the intersection of a decreasing sequence of sets lies outside K (k + 1) for some k.

theorem TauCeti.exists_map_eq_of_notMem {α : Type u_1} {β : Type u_2} {K : ℕ → Set α} (hKsucc : ∀ (i : ℕ), K (i + 1) ⊆ K i) {G : ℕ → α → β} (hGstab : ∀ (k m : ℕ), k ≤ m → ∀ x ∉ K (k + 1), G m x = G k x) (q : β) : ∃ (g : α → β), (∀ x ∈ ⋂ (i : ℕ), K i, g x = q) ∧ ∀ (k : ℕ), ∀ x ∉ K (k + 1), g x = G k x

Let K₀ ⊇ K₁ ⊇ ⋯ be a decreasing sequence of sets, and G k maps such that G m = G k outside K (k + 1) whenever k ≤ m. For every q there is a map g with value q on ⋂ i, K i which agrees with G k outside K (k + 1) for every k.