Theorems · Theorem · order theory
Set.pi_def
∀ {α : Type u_1} {π : α → Type u_12} (i : Set α) (s : (a : α) → Set (π a)), i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Set.extproof · cited by 2,266
- Set.iInterstatement · cited by 1,084
- Set.pistatement · cited by 405
- Function.evalstatement · cited by 140
Cited by14
Results whose statement or proof uses this declaration.
- MeasurableSet.piproof · cited by 14
- set_pi_mem_nhdsproof · cited by 11
- isOpen_set_piproof · cited by 8
- Filter.mem_piproof · cited by 8
- isClosed_set_piproof · cited by 5
- Filter.hasBasis_piproof · cited by 5
- Filter.pi_mem_piproof · cited by 4
- Set.univ_pi_eq_iInterproof · cited by 2
- isTopologicalBasis_piproof · cited by 2
- nhdsWithin_pi_eqproof · cited by 1
- Set.iUnion_pi_of_monotoneproof · cited by 1
- Filter.ker_piproof · cited by 1