Theorems · Theorem · order theory

Set.iUnionLift_unary

∀ {α : 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) (u : ↑T → ↑T) (ui : (i : ι) → ↑(S i) → ↑(S i)),
  (∀ (i : ι) (x : ↑(S i)), u (Set.inclusion ⋯ x) = Set.inclusion ⋯ (ui i x)) →
    ∀ (uβ : β → β),
      (∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)) →
        ∀ (x : ↑T), Set.iUnionLift S f hf T ⋯ (u x) = uβ (Set.iUnionLift S f hf T ⋯ x)

iUnionLift_unary 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 LinearMaps on a union of submodules preserves scalar multiplication.

Defined in

Mathlib.Data.Set.UnionLift

Cited by

0 results in Mathlib

Foundations

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