Pi

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems pi, pi, pi_eq_generateFrom_projections, generateFrom_eq_pi, generateFrom_pi, generateFrom_pi_eq, isPiSystem_pi	7
Total	7

IsCountablySpanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	IsCountablySpanning	Set.image Set Set.pi Set.univ	—	nonempty_encodable instCountableForallOfFinite instCountableNat Set.mem_image_of_mem Function.Surjective.iUnion_comp Encodable.surjective_decode_getD Set.iUnion_univ_pi Set.pi_univ

IsPiSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	IsPiSystem	Set.image Set Set.pi Set.univ	—	Set.pi_inter_distrib Set.mem_image_of_mem Set.mem_univ Set.univ_pi_nonempty_iff

MeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_eq_generateFrom_projections 📖	mathematical	—	pi generateFrom setOf Set MeasurableSet Set.preimage Function.eval	—	Set.iUnion_setOf

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generateFrom_eq_pi 📖	mathematical	MeasurableSpace.generateFrom IsCountablySpanning	Set.image Set Set.pi Set.univ MeasurableSpace.pi	—	generateFrom_pi_eq
generateFrom_pi 📖	mathematical	—	MeasurableSpace.generateFrom Set.image Set Set.pi Set.univ setOf MeasurableSet MeasurableSpace.pi	—	generateFrom_eq_pi MeasurableSpace.generateFrom_measurableSet isCountablySpanning_measurableSet
generateFrom_pi_eq 📖	mathematical	IsCountablySpanning	MeasurableSpace.pi MeasurableSpace.generateFrom Set.image Set Set.pi Set.univ	—	nonempty_encodable Finite.to_countable le_antisymm iSup_le MeasurableSpace.comap_generateFrom MeasurableSpace.generateFrom_le Set.eval_preimage Set.iUnion_const Set.ext Function.update_self Function.update_of_ne Set.iUnion_univ_pi MeasurableSet.iUnion instCountableForallOfFinite instCountableNat MeasurableSpace.measurableSet_generateFrom Set.mem_image_of_mem Set.univ_pi_eq_iInter MeasurableSet.iInter Encodable.countable measurable_pi_apply Set.mem_univ
isPiSystem_pi 📖	mathematical	—	IsPiSystem Set.image Set Set.pi Set.univ setOf MeasurableSet	—	IsPiSystem.pi MeasurableSpace.isPiSystem_measurableSet

---

← Back to Index