Theorems · Theorem · order theory

Set.iUnionLift_binary

∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  (hT' : T = Set.iUnion S),
  Directed (fun x1 x2 => x1 ⊆ x2) S →
    ∀ (op : ↑T → ↑T → ↑T) (opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)),
      (∀ (i : ι) (x y : ↑(S i)), Set.inclusion ⋯ (opi i x y) = op (Set.inclusion ⋯ x) (Set.inclusion ⋯ y)) →
        ∀ (opβ : β → β → β),
          (∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)) →
            ∀ (x y : ↑T),
              Set.iUnionLift S f hf T ⋯ (op x y) = opβ (Set.iUnionLift S f hf T ⋯ x) (Set.iUnionLift S f hf T ⋯ y)

iUnionLift_binary is useful for proving that iUnionLift is a homomorphism of algebraic structures when defined on the Union of algebraic subobjects. For example, it could be used to prove that the lift of a collection of group homomorphisms on a union of subgroups preserves *.

Defined in

Mathlib.Data.Set.UnionLift

Cited by

0 results in Mathlib

Foundations

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