Theorems · Theorem · order theory

Set.preimage_iUnionLift

∀ {α : Type u_1} {ι : Sort u_3} {β : Type 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} (t : Set β),
  Set.iUnionLift S f hf T hT ⁻¹' t = Set.inclusion hT ⁻¹' ⋃ i, Set.inclusion ⋯ '' f i ⁻¹' t

Defined in

Mathlib.Data.Set.UnionLift

Cited by

2 results in Mathlib

Foundations

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