rainbow.math.finite.set-union

set/infinite-indexed-union-member

TheoremFor all inputsNo axiomsSource, line 51

set/infinite-indexed-union-member.{u, i} :
  (A : Type u) (Index : Sort i) (family : Index → set/Set A) (index : Index)
  (infinite-evidence : set/infinite A (family index))
  → set/infinite A (set/indexed-union A Index family)

set/infinite-indexed-union2-member

TheoremFor all inputsNo axiomsSource, line 110

set/infinite-indexed-union2-member.{u, i, j} :
  (A : Type u) (Index : Sort i) (Second : ∀ (index : Index), Sort j)
  (family : ∀ (index : Index), ∀ (second : Second index), set/Set A) (index : Index)
  (second : Second index) (infinite-evidence : set/infinite A (family index second))
  → set/infinite A (union)
  where union := set/indexed-union A Index (fun outer => set/indexed-union A (Second outer) (fun inner => family outer inner))

set/infinite-union-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 158

set/infinite-union-equivalence.{u} :
  (A : Type u) (left right : set/Set A)
  → proposition/conjunction (set/infinite A (set/union A left right) → disjunction) (disjunction → set/infinite A (set/union A left right))
  where disjunction := proposition/disjunction (set/infinite A left) (set/infinite A right)

set/finite-singleton-equivalence

TheoremFor all inputsNo axiomsSource, line 242

set/finite-singleton-equivalence.{u} :
  (A : Type u) (selected : A)
  → proposition/conjunction (set/finite A (set/singleton A selected) → proposition/truth) (proposition/truth → set/finite A (set/singleton A selected))

set/finite-singleton-proposition-equality

TheoremFor all inputsAxioms: sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 263

set/finite-singleton-proposition-equality.{u} :
  (A : Type u) (selected : A)
  → set/finite A (set/singleton A selected) = proposition/truth

= = equality/Eq