Documentation Verification Report

Lattice

📁 Source: Mathlib/MeasureTheory/Order/Lattice.lean

Statistics

Metric	Count
Definitions `MeasurableInf`, `MeasurableInf₂`, `MeasurableSup`, `MeasurableSup₂`	4
Theorems `const_inf`, `const_sup`, `inf`, `inf'`, `inf_const`, `sup`, `sup'`, `sup_const`, `measurable_range_sup'`, `measurable_range_sup''`, `measurable_sup'`, `const_inf`, `const_sup`, `inf`, `inf'`, `inf_const`, `sup`, `sup'`, `sup_const`, `measurable_const_inf`, `measurable_inf_const`, `measurable_inf`, `to_hasMeasurableInf`, `measurable_const_sup`, `measurable_sup_const`, `measurable_sup`, `toMeasurableSup`, `instMeasurableInf`, `instMeasurableInf₂`, `instMeasurableSup`, `instMeasurableSup₂`	31
Total	35

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_inf` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableInf.measurable_const_inf`
`const_sup` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableSup.measurable_const_sup`
`inf` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableInf₂.measurable_inf` `prodMk`
`inf'` 📖	mathematical	`AEMeasurable`	`Pi.instMinForall_mathlib`	—	`Measurable.comp_aemeasurable` `MeasurableInf₂.measurable_inf` `prodMk`
`inf_const` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableInf.measurable_inf_const`
`sup` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableSup₂.measurable_sup` `prodMk`
`sup'` 📖	mathematical	`AEMeasurable`	`Pi.instMaxForall_mathlib`	—	`Measurable.comp_aemeasurable` `MeasurableSup₂.measurable_sup` `prodMk`
`sup_const` 📖	—	`AEMeasurable`	—	—	`Measurable.comp_aemeasurable` `MeasurableSup.measurable_sup_const`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_range_sup'` 📖	mathematical	`Measurable`	`sup'` `Pi.instSemilatticeSup` `range` `nonempty_range_add_one`	—	`measurable_sup'` `nonempty_range_add_one` `Nat.instNoMaxOrder`
`measurable_range_sup''` 📖	mathematical	`Measurable`	`sup'` `range` `nonempty_range_add_one`	—	`nonempty_range_add_one` `sup'_apply` `measurable_range_sup'`
`measurable_sup'` 📖	mathematical	`Nonempty` `Measurable`	`sup'` `Pi.instSemilatticeSup`	—	`sup'_induction` `Measurable.sup`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_inf` 📖	—	`Measurable`	—	—	`comp` `MeasurableInf.measurable_const_inf`
`const_sup` 📖	—	`Measurable`	—	—	`comp` `MeasurableSup.measurable_const_sup`
`inf` 📖	—	`Measurable`	—	—	`comp` `MeasurableInf₂.measurable_inf` `prodMk`
`inf'` 📖	mathematical	`Measurable`	`Pi.instMinForall_mathlib`	—	`comp` `MeasurableInf₂.measurable_inf` `prodMk`
`inf_const` 📖	—	`Measurable`	—	—	`comp` `MeasurableInf.measurable_inf_const`
`sup` 📖	—	`Measurable`	—	—	`comp` `MeasurableSup₂.measurable_sup` `prodMk`
`sup'` 📖	mathematical	`Measurable`	`Pi.instMaxForall_mathlib`	—	`comp` `MeasurableSup₂.measurable_sup` `prodMk`
`sup_const` 📖	—	`Measurable`	—	—	`comp` `MeasurableSup.measurable_sup_const`

MeasurableInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_const_inf` 📖	mathematical	—	`Measurable`	—	—
`measurable_inf_const` 📖	mathematical	—	`Measurable`	—	—

MeasurableInf₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_inf` 📖	mathematical	—	`Measurable` `Prod.instMeasurableSpace`	—	—
`to_hasMeasurableInf` 📖	mathematical	—	`MeasurableInf`	—	`Measurable.inf` `measurable_const` `measurable_id'`

MeasurableSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_const_sup` 📖	mathematical	—	`Measurable`	—	—
`measurable_sup_const` 📖	mathematical	—	`Measurable`	—	—

MeasurableSup₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_sup` 📖	mathematical	—	`Measurable` `Prod.instMeasurableSpace`	—	—
`toMeasurableSup` 📖	mathematical	—	`MeasurableSup`	—	`Measurable.sup` `measurable_const` `measurable_id'`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMeasurableInf` 📖	mathematical	—	`MeasurableInf` `OrderDual` `instMeasurableSpaceOrderDual` `instInf`	—	`MeasurableSup.measurable_const_sup` `MeasurableSup.measurable_sup_const`
`instMeasurableInf₂` 📖	mathematical	—	`MeasurableInf₂` `OrderDual` `instMeasurableSpaceOrderDual` `instInf`	—	`MeasurableSup₂.measurable_sup`
`instMeasurableSup` 📖	mathematical	—	`MeasurableSup` `OrderDual` `instMeasurableSpaceOrderDual` `instSup`	—	`MeasurableInf.measurable_const_inf` `MeasurableInf.measurable_inf_const`
`instMeasurableSup₂` 📖	mathematical	—	`MeasurableSup₂` `OrderDual` `instMeasurableSpaceOrderDual` `instSup`	—	`MeasurableInf₂.measurable_inf`

(root)

Definitions

Name	Category	Theorems
`MeasurableInf` 📖	CompData	3 math math: `ContinuousInf.measurableInf`, `OrderDual.instMeasurableInf`, `MeasurableInf₂.to_hasMeasurableInf`
`MeasurableInf₂` 📖	CompData	2 math math: `OrderDual.instMeasurableInf₂`, `ContinuousInf.measurableInf₂`
`MeasurableSup` 📖	CompData	3 math math: `MeasurableSup₂.toMeasurableSup`, `OrderDual.instMeasurableSup`, `ContinuousSup.measurableSup`
`MeasurableSup₂` 📖	CompData	2 math math: `OrderDual.instMeasurableSup₂`, `ContinuousSup.measurableSup₂`

---

← Back to Index