Theorems · Definition · order theory

Set.iUnionLift

{α : 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⟩) →
            (T : Set α) → T ⊆ Set.iUnion S → ↑T → β

Given a union of sets iUnion S, define a function on the Union by defining it on each component, and proving that it agrees on the intersections.

Defined in

Mathlib.Data.Set.UnionLift

Cited by

11 results in Mathlib

Foundations

Depth 10 from the axioms · uses Classical.choice