Theorems · Theorem · order theory

Set.iUnion_image_left

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β},
  ⋃ a ∈ s, f a '' t = Set.image2 f s t

Defined in: Mathlib.Data.Set.Lattice.Image
Cited by: 15 results in Mathlib
Foundations: Depth 10 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.imagestatement · cited by 5,609
Set.iUnionstatement and proof · cited by 2,483
Set.iUnion_congr_Propproof · cited by 374
Set.image2statement · cited by 311
Set.image_eq_iUnionproof · cited by 2
Set.image2_eq_iUnionproof · cited by 1

Cited by15

Results whose statement or proof uses this declaration.

Set.iUnion_image_rightproof · cited by 15
Set.iUnion_vadd_setproof · cited by 10
Set.iUnion_smul_setproof · cited by 7
Finset.biUnion_image_leftproof · cited by 5
Set.iUnion_smul_left_imageproof · cited by 2
Set.iUnion_div_left_imageproof · cited by 1
Set.iUnion_vadd_left_imageproof · cited by 1
Set.iUnion_mul_left_imageproof · cited by 1
Set.iUnion_add_left_imageproof · cited by 1
Set.iUnion_sub_left_imageproof · cited by 1
Set.iUnion_image_inf_leftproof · cited by 0
Set.iUnion_image_sup_leftproof · cited by 0