Documentation Verification Report

RCLike

📁 Source: Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean

Statistics

Metric	Count
Definitions `RCLike`	1
Theorems `im`, `re`, `im`, `re`, `measurable_im`, `measurable_ofReal`, `measurable_re`, `aemeasurable_of_re_im`, `measurable_of_re_im`	9
Total	10

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`im` 📖	mathematical	`AEMeasurable` `RCLike.measurableSpace`	`AEMeasurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.im`	—	`Measurable.comp_aemeasurable` `RCLike.measurable_im`
`re` 📖	mathematical	`AEMeasurable` `RCLike.measurableSpace`	`AEMeasurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re`	—	`Measurable.comp_aemeasurable` `RCLike.measurable_re`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`im` 📖	mathematical	`Measurable` `RCLike.measurableSpace`	`Measurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.im`	—	`comp` `RCLike.measurable_im`
`re` 📖	mathematical	`Measurable` `RCLike.measurableSpace`	`Measurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re`	—	`comp` `RCLike.measurable_re`

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_im` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `im`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `Real.borelSpace` `continuous_im`
`measurable_ofReal` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `measurableSpace` `ofReal`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `borelSpace` `continuous_ofReal`
`measurable_re` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `re`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `Real.borelSpace` `continuous_re`

(root)

Definitions

Name	Category	Theorems
`RCLike` 📖	CompData	1 math math: `IsRCLikeNormedField.out`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aemeasurable_of_re_im` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `RCLike.im`	`AEMeasurable` `RCLike.measurableSpace`	—	`RCLike.re_add_im` `AEMeasurable.add` `ContinuousAdd.measurableMul₂` `RCLike.borelSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.comp_aemeasurable` `RCLike.measurable_ofReal` `AEMeasurable.mul_const` `ContinuousMul.measurableMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`measurable_of_re_im` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `RCLike.im`	`Measurable` `RCLike.measurableSpace`	—	`RCLike.re_add_im` `Measurable.add` `ContinuousAdd.measurableMul₂` `RCLike.borelSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.comp` `RCLike.measurable_ofReal` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`

---

← Back to Index