rainbow.math.finite.set-indexed-union

set/list-indexed-union

DefinitionSource, line 58

set/list-indexed-union.{u, v} :
  (A : Type u) (Index : Type v) (family : Index → set/Set A) (x₁ : List Index)
  → set/Set A

List = data/List

set/restricted-indexed-union

DefinitionSource, line 83

set/restricted-indexed-union.{u, v} :
  (A : Type u) (Index : Type v) (indices : set/Set Index) (family : Index → set/Set A)
  → set/Set A

set/restricted-indexed-union-member

TheoremFor all inputsNo axiomsSource, line 108

set/restricted-indexed-union-member.{u, v} :
  (A : Type u) (Index : Type v) (indices : set/Set Index) (family : Index → set/Set A)
  (index : Index) (index-member : indices index) (value : A)
  (value-member : family index value)
  → set/restricted-indexed-union A Index indices family value

set/list-indexed-union-member

TheoremFor all inputsNo axiomsSource, line 155

set/list-indexed-union-member.{u, v} :
  (A : Type u) (Index : Type v) (family : Index → set/Set A) (source : List Index)
  (index : Index) (index-member : list/membership Index source index) (value : A)
  (value-member : family index value)
  → set/list-indexed-union A Index family source value

List = data/List

set/finite-list-indexed-union

TheoremFor all inputsNo axiomsSource, line 245

set/finite-list-indexed-union.{u, v} :
  (A : Type u) (Index : Type v) (family : Index → set/Set A)
  (family-finite : ∀ (index : Index), set/finite A (family index)) (source : List Index)
  → (fun source₁ => set/finite A (set/list-indexed-union A Index family source₁)) source

List = data/List

set/restricted-indexed-union-subset-list

TheoremFor all inputsNo axiomsSource, line 307

set/restricted-indexed-union-subset-list.{u, v} :
  (A : Type u) (Index : Type v) (indices : set/Set Index) (family : Index → set/Set A)
  (enumeration : List Index)
  (index-cover : ∀ (index : Index), ∀ (member : indices index), list/membership Index enumeration index)
  → set/subset A (union) (union₁)
  where union := set/restricted-indexed-union A Index indices family
  where union₁ := set/list-indexed-union A Index family enumeration

List = data/List

set/finite-restricted-indexed-union

TheoremFor all inputsNo axiomsSource, line 379

set/finite-restricted-indexed-union.{u, v} :
  (A : Type u) (Index : Type v) (indices : set/Set Index) (family : Index → set/Set A)
  (indices-finite : set/finite Index indices)
  (family-finite : ∀ (index : Index), set/finite A (family index))
  → set/finite A (union)
  where union := set/restricted-indexed-union A Index indices family

set/restricted-indexed-union-subset

TheoremFor all inputsNo axiomsSource, line 307

set/restricted-indexed-union-subset.{u, v} :
  (A : Type u) (Index : Type v) (indices : set/Set Index) (family : Index → set/Set A)
  → set/subset A (union) (set/indexed-union A Index family)
  where union := set/restricted-indexed-union A Index indices family

set/indexed-union-subset-universal-restricted

TheoremFor all inputsNo axiomsSource, line 474

set/indexed-union-subset-universal-restricted.{u, v} :
  (A : Type u) (Index : Type v) (family : Index → set/Set A)
  → set/subset A (set/indexed-union A Index family) (union)
  where union := set/restricted-indexed-union A Index (set/universal Index) family

set/finite-indexed-union

TheoremFor all inputsNo axiomsSource, line 519

set/finite-indexed-union.{u, v} :
  (A : Type u) (Index : Type v) (family : Index → set/Set A)
  (index-type-finite : set/finite Index (set/universal Index))
  (family-finite : ∀ (index : Index), set/finite A (family index))
  → set/finite A (set/indexed-union A Index family)