Theorems · Theorem · order theory
Set.preimage_compl
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ- Defined in
- Mathlib.Data.Set.Image
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.preimagestatement · cited by 4,946
- Compl.complstatement · cited by 2,925
Cited by43
Results whose statement or proof uses this declaration.
- MeasurableEmbedding.map_applyproof · cited by 16
- Set.kernImage_eq_complproof · cited by 9
- t1Space_TFAEproof · cited by 8
- Topology.IsClosedEmbedding.of_continuous_injective_isClosedMapproof · cited by 7
- measurable_of_isClosedproof · cited by 4
- isInducing_stoneCechUnitproof · cited by 4
- preconnectedSpace_iff_clopenproof · cited by 3
- meromorphicNFAt_smul_iff_right_of_analyticAtproof · cited by 3
- Topology.IsConstructible.preimageproof · cited by 3
- Ergodic.of_mem_extremePoints_measure_univ_eqproof · cited by 2
- Set.compl_negproof · cited by 2