Theorems · Theorem · order theory

Set.iUnionLift_const

∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {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} (c : ↑T) (ci : (i : ι) → ↑(S i)),
  (∀ (i : ι), ↑(ci i) = ↑c) → ∀ (cβ : β), (∀ (i : ι), f i (ci i) = cβ) → Set.iUnionLift S f hf T hT c = cβ

iUnionLift_const 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 1.

Defined in

Mathlib.Data.Set.UnionLift

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses Classical.choice