Mathlib Map

Theorems · Definition · order theory

memPartitionSet

{α : Type u_1} → (ℕ → Set α) → ℕ → α → Set α

The set in memPartition f n to which a : α belongs.

Defined in
Mathlib.Data.Set.MemPartition
Cited by
12 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasurableSpace.countablePartitionSet · cited by 24MeasurableSpace.countable…memPartitionSet_mem · cited by 5memPartitionSet_memmemPartitionSet_eq_iff · cited by 3memPartitionSet_eq_iffmemPartitionSet_succ · cited by 2memPartitionSet_succProbabilityTheory.measurable_memPartitionSet_subtype · cited by 2ProbabilityTheory.measura…mem_memPartitionSet · cited by 2mem_memPartitionSetmemPartitionSet_of_mem · cited by 1memPartitionSet_of_memProbabilityTheory.measurable_partitionFiltration_memPartitionSet · cited by 1ProbabilityTheory.measura…memPartitionSet_zero · cited by 0memPartitionSet_zeromemPartitionSet.eq_def · cited by 0memPartitionSet.eq_defProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet · cited by 0ProbabilityTheory.measura…ProbabilityTheory.measurable_memPartitionSet · cited by 0ProbabilityTheory.measura…MeasurableSpace.measurableSet_memPartitionSet · cited by 0MeasurableSpace.measurabl…Set · cited by 53352SetmemPartitionSetCITED BYCITES

Cites1

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

Cited by13

Results whose statement or proof uses this declaration.