Documentation Verification Report

BaireMeasurable

📁 Source: Mathlib/Topology/Baire/BaireMeasurable.lean

Statistics

Metric	Count
Definitions `BaireMeasurableSet`, `«term_=ᵇ_»`, `«term∀ᵇ_,_»`, `«term∃ᵇ_,_»`	4
Theorems `biInter`, `biUnion`, `compl`, `diff`, `iInter`, `iUnion`, `iff_residualEq_isOpen`, `inter`, `of_compl`, `of_mem_residual`, `preimage`, `residualEq_isOpen`, `sInter`, `sUnion`, `union`, `residual_map_eq`, `baireMeasurableSet`, `preimage_of_isOpenMap`, `baireMeasurableSet`, `baireMeasurableSet`, `residualEq_isOpen`, `closure_residualEq`, `coborder_mem_residual`, `tendsto_residual_of_isOpenMap`	24
Total	28

BaireMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter` 📖	mathematical	`BaireMeasurableSet`	`Set.iInter` `Set` `Set.instMembership`	—	`MeasurableSet.biInter` `countableInterFilter_residual`
`biUnion` 📖	mathematical	`BaireMeasurableSet`	`Set.iUnion` `Set` `Set.instMembership`	—	`MeasurableSet.biUnion` `countableInterFilter_residual`
`compl` 📖	mathematical	`BaireMeasurableSet`	`Compl.compl` `Set` `Set.instCompl`	—	`MeasurableSet.compl` `countableInterFilter_residual`
`diff` 📖	mathematical	`BaireMeasurableSet`	`Set` `Set.instSDiff`	—	`MeasurableSet.diff` `countableInterFilter_residual`
`iInter` 📖	mathematical	`BaireMeasurableSet`	`Set.iInter`	—	`MeasurableSet.iInter` `countableInterFilter_residual`
`iUnion` 📖	mathematical	`BaireMeasurableSet`	`Set.iUnion`	—	`MeasurableSet.iUnion` `countableInterFilter_residual`
`iff_residualEq_isOpen` 📖	mathematical	—	`BaireMeasurableSet` `IsOpen` `Filter.EventuallyEq` `residual`	—	`residualEq_isOpen` `congr` `IsOpen.baireMeasurableSet` `Filter.EventuallyEq.symm`
`inter` 📖	mathematical	`BaireMeasurableSet`	`Set` `Set.instInter`	—	`MeasurableSet.inter` `countableInterFilter_residual`
`of_compl` 📖	—	`BaireMeasurableSet` `Compl.compl` `Set` `Set.instCompl`	—	—	`MeasurableSet.of_compl` `countableInterFilter_residual`
`of_mem_residual` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `residual`	`BaireMeasurableSet`	—	`eventuallyMeasurableSet_of_mem_filter` `countableInterFilter_residual`
`preimage` 📖	mathematical	`Continuous` `IsOpenMap` `BaireMeasurableSet`	`Set.preimage`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Filter.EventuallyEq.filter_mono` `tendsto_residual_of_isOpenMap`
`residualEq_isOpen` 📖	mathematical	`BaireMeasurableSet`	`IsOpen` `Filter.EventuallyEq` `residual`	—	`MeasurableSet.residualEq_isOpen` `Filter.EventuallyEq.trans`
`sInter` 📖	mathematical	`BaireMeasurableSet`	`Set.sInter`	—	`MeasurableSet.sInter` `countableInterFilter_residual`
`sUnion` 📖	mathematical	`BaireMeasurableSet`	`Set.sUnion`	—	`MeasurableSet.sUnion` `countableInterFilter_residual`
`union` 📖	mathematical	`BaireMeasurableSet`	`Set` `Set.instUnion`	—	`MeasurableSet.union` `countableInterFilter_residual`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`residual_map_eq` 📖	mathematical	—	`Filter.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `residual`	—	`le_antisymm` `tendsto_residual_of_isOpenMap` `continuous` `isOpenMap` `Filter.le_map`

IsMeagre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baireMeasurableSet` 📖	mathematical	`IsMeagre`	`BaireMeasurableSet`	—	`BaireMeasurableSet.of_compl` `BaireMeasurableSet.of_mem_residual`
`preimage_of_isOpenMap` 📖	mathematical	`Continuous` `IsOpenMap` `IsMeagre`	`Set.preimage`	—	`tendsto_residual_of_isOpenMap`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baireMeasurableSet` 📖	mathematical	`IsOpen`	`BaireMeasurableSet`	—	`MeasurableSet.baireMeasurableSet` `measurableSet` `BorelSpace.opensMeasurable`

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baireMeasurableSet` 📖	mathematical	`MeasurableSet`	`BaireMeasurableSet`	—	`BorelSpace.measurable_eq` `eventuallyMeasurableSet` `countableInterFilter_residual`
`residualEq_isOpen` 📖	mathematical	`MeasurableSet`	`IsOpen` `Filter.EventuallyEq` `residual`	—	`induction_on_open` `Filter.EventuallyEq.rfl` `IsClosed.isOpen_compl` `isClosed_closure` `Filter.EventuallyEq.compl` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `closure_residualEq` `IsOpen.isLocallyClosed` `isOpen_iUnion` `EventuallyEq.countable_iUnion` `countableInterFilter_residual` `instCountableNat`

Topology

Definitions

Name	Category	Theorems
`«term_=ᵇ_»` 📖	CompOp	—
`«term∀ᵇ_,_»` 📖	CompOp	—
`«term∃ᵇ_,_»` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`BaireMeasurableSet` 📖	MathDef	5 math math: `BaireMeasurableSet.of_mem_residual`, `IsMeagre.baireMeasurableSet`, `MeasurableSet.baireMeasurableSet`, `BaireMeasurableSet.iff_residualEq_isOpen`, `IsOpen.baireMeasurableSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_residualEq` 📖	mathematical	`IsLocallyClosed`	`Filter.EventuallyEq` `residual` `closure`	—	`Filter.eventuallyEq_set` `Filter.mp_mem` `coborder_mem_residual` `Filter.univ_mem'` `closure_inter_coborder`
`coborder_mem_residual` 📖	mathematical	`IsLocallyClosed`	`Set` `Filter` `Filter.instMembership` `residual` `coborder`	—	`residual_of_dense_open` `IsLocallyClosed.isOpen_coborder` `dense_coborder`
`tendsto_residual_of_isOpenMap` 📖	mathematical	`Continuous` `IsOpenMap`	`Filter.Tendsto` `residual`	—	`Filter.le_countableGenerate_iff_of_countableInterFilter` `instCountableInterFilterMap` `countableInterFilter_residual` `residual_of_dense_open` `IsOpen.preimage` `Dense.preimage`

---

← Back to Index