Theorems · Definition · order theory

Set.liftCover

{α : Type u_1} →
  {ι : Sort u_2} →
    {β : Sort u_3} →
      (S : ι → Set α) →
        (f : (i : ι) → ↑(S i) → β) →
          (∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) →
            Set.iUnion S = Set.univ → α → β

Glue together functions defined on each of a collection S of sets that cover a type. See also Set.iUnionLift.

Defined in

Mathlib.Data.Set.UnionLift

Cited by

7 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound