Theorems · Theorem · order theory
Set.image_iInter
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β},
Function.Bijective f → ∀ (s : ι → Set α), f '' ⋂ i, s i = ⋂ i, f '' s i- Defined in
- Mathlib.Data.Set.Lattice.Image
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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 and proof · cited by 5,609
- Set.univproof · cited by 3,945
- Set.iInterstatement · cited by 1,084
- Function.Bijectivestatement and proof · cited by 863
- IsEmptyproof · cited by 759
- Function.Injective.injOnproof · cited by 280
- isEmpty_or_nonemptyproof · cited by 269
- Function.Bijective.injectiveproof · cited by 115
- Function.Bijective.surjectiveproof · cited by 114
- Set.iInter_of_emptyproof · cited by 23
- Set.InjOn.image_iInter_eqproof · cited by 22
Cited by4
Results whose statement or proof uses this declaration.
- Set.smul_set_iInterproof · cited by 1
- Set.vadd_set_iInterproof · cited by 1
- cantorSet_eq_union_halvesproof · cited by 1
- Set.image_iInter₂proof · cited by 0