CompMap

Statistics

Metric	Count
Definitions	0
Theorems `comp_deterministic_eq_comap`, `comp_map`, `deterministic_comp_deterministic`, `deterministic_comp_eq_map`, `fst_comp`, `map_comp`, `snd_comp`, `swap_comp_eq_map`, `swap_swap`	9
Total	9

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_deterministic_eq_comap` 📖	mathematical	`Measurable`	`comp` `deterministic` `comap`	—	`ext` `MeasureTheory.Measure.ext` `comap_apply'` `comp_apply'` `MeasureTheory.lintegral_dirac'` `measurable_coe`
`comp_map` 📖	mathematical	`Measurable`	`comp` `map` `comap`	—	`ext` `MeasureTheory.Measure.ext` `comp_apply'` `lintegral_map` `measurable_coe`
`deterministic_comp_deterministic` 📖	mathematical	`Measurable`	`comp` `deterministic` `Measurable.comp`	—	`ext` `Measurable.comp` `MeasureTheory.Measure.ext` `comp_deterministic_eq_comap`
`deterministic_comp_eq_map` 📖	mathematical	`Measurable`	`comp` `deterministic` `map`	—	`ext` `MeasureTheory.Measure.ext` `map_apply'` `comp_apply'` `deterministic_apply'` `MeasureTheory.lintegral_indicator_const_comp` `one_mul`
`fst_comp` 📖	mathematical	—	`fst` `comp` `Prod.instMeasurableSpace`	—	`fst_eq` `map_comp`
`map_comp` 📖	mathematical	—	`map` `comp`	—	`ext` `MeasureTheory.Measure.ext` `map_apply'` `comp_apply'` `map_of_not_measurable` `zero_comp`
`snd_comp` 📖	mathematical	—	`snd` `comp` `Prod.instMeasurableSpace`	—	`snd_eq` `map_comp`
`swap_comp_eq_map` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `swap` `map`	—	`measurable_swap` `swap.eq_1` `deterministic_comp_eq_map`
`swap_swap` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `swap` `id`	—	`measurable_swap` `Measurable.comp` `deterministic_comp_deterministic` `deterministic.congr_simp`

---