Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/GDelta/Basic.lean

Statistics

Metric	Count
Definitions `IsGδ`, `IsMeagre`, `IsNowhereDense`, `residual`	4
Theorems `isNowhereDense_iff`, `biInter`, `biInter_of_isOpen`, `biUnion`, `empty`, `eq_iInter_nat`, `iInter`, `iInter_of_isOpen`, `iUnion`, `inter`, `sInter`, `sUnion`, `union`, `univ`, `empty`, `image_val`, `inter`, `mono`, `union`, `closure`, `image_val`, `isMeagre`, `mono`, `subset_of_closed_isNowhereDense`, `isGδ`, `isMeagre_image`, `isNowhereDense_image`, `countableInterFilter_residual`, `exists_of_not_isMeagre_biUnion`, `isClosed_isNowhereDense_iff_compl`, `isGδ_iff_eq_iInter_nat`, `isGδ_induced`, `isMeagre_biUnion`, `isMeagre_iUnion`, `isMeagre_iff_countable_union_isNowhereDense`, `isNowhereDense_empty`, `isNowhereDense_iff_disjoint`, `isNowhereDense_iff_forall_notMem_nhds`, `mem_residual_iff`, `nonempty_of_not_isMeagre`, `residual_of_dense_Gδ`, `residual_of_dense_open`	42
Total	46

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNowhereDense_iff` 📖	mathematical	—	`IsNowhereDense` `interior` `Set` `Set.instEmptyCollection`	—	`IsNowhereDense.eq_1` `closure_eq`

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter` 📖	mathematical	`IsGδ`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.biInter_eq_iInter` `iInter` `Set.Countable.to_subtype`
`biInter_of_isOpen` 📖	mathematical	`IsOpen`	`IsGδ` `Set.iInter` `Set` `Set.instMembership`	—	`Set.forall_mem_image` `Set.Countable.image` `Set.sInter_image`
`biUnion` 📖	mathematical	`IsGδ`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_image` `sUnion` `Set.Finite.image` `Set.forall_mem_image`
`empty` 📖	mathematical	—	`IsGδ` `Set` `Set.instEmptyCollection`	—	`IsOpen.isGδ` `isOpen_empty`
`eq_iInter_nat` 📖	mathematical	`IsGδ`	`IsOpen` `Set.iInter`	—	`isGδ_iff_eq_iInter_nat`
`iInter` 📖	mathematical	`IsGδ`	`Set.iInter`	—	`forall_swap` `Set.countable_iUnion` `Set.sInter_iUnion`
`iInter_of_isOpen` 📖	mathematical	`IsOpen`	`IsGδ` `Set.iInter`	—	`Set.forall_mem_range` `Set.countable_range` `Set.sInter_range`
`iUnion` 📖	mathematical	`IsGδ`	`Set.iUnion`	—	`sUnion` `Set.finite_range` `Set.forall_mem_range`
`inter` 📖	mathematical	`IsGδ`	`Set` `Set.instInter`	—	`Set.inter_eq_iInter` `iInter` `Bool.countable`
`sInter` 📖	mathematical	`IsGδ`	`Set.sInter`	—	`Set.sInter_eq_biInter` `biInter`
`sUnion` 📖	mathematical	`IsGδ`	`Set.sUnion`	—	`Set.Finite.induction_on` `Set.sUnion_empty` `Set.sUnion_insert` `union`
`union` 📖	mathematical	`IsGδ`	`Set` `Set.instUnion`	—	`Set.sInter_union_sInter` `biInter_of_isOpen` `Set.Countable.prod` `IsOpen.union`
`univ` 📖	mathematical	—	`IsGδ` `Set.univ`	—	`IsOpen.isGδ` `isOpen_univ`

IsMeagre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty` 📖	mathematical	—	`IsMeagre` `Set` `Set.instEmptyCollection`	—	`eq_1` `Set.compl_empty` `Filter.univ_mem`
`image_val` 📖	mathematical	`IsMeagre` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`Set.image`	—	`Topology.IsInducing.isMeagre_image` `Topology.IsInducing.subtypeVal`
`inter` 📖	mathematical	`IsMeagre`	`Set` `Set.instInter`	—	`mono` `Set.inter_subset_left`
`mono` 📖	—	`Set` `Set.instHasSubset` `IsMeagre`	—	—	`Filter.mem_of_superset` `Set.compl_subset_compl`
`union` 📖	mathematical	`IsMeagre`	`Set` `Set.instUnion`	—	`eq_1` `Set.compl_union` `Filter.inter_mem`

IsNowhereDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`IsNowhereDense`	`closure`	—	`eq_1` `closure_closure`
`image_val` 📖	mathematical	`IsNowhereDense` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`Set.image`	—	`Topology.IsInducing.isNowhereDense_image` `Topology.IsInducing.subtypeVal`
`isMeagre` 📖	mathematical	`IsNowhereDense`	`IsMeagre`	—	`isMeagre_iff_countable_union_isNowhereDense` `Set.sUnion_singleton` `Set.instReflSubset`
`mono` 📖	—	`Set` `Set.instHasSubset` `IsNowhereDense`	—	—	`Set.eq_empty_of_subset_empty` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `interior_mono` `closure_mono` `subset_refl` `Set.instReflSubset`
`subset_of_closed_isNowhereDense` 📖	mathematical	`IsNowhereDense`	`Set` `Set.instHasSubset` `IsClosed`	—	`subset_closure` `closure` `isClosed_closure`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGδ` 📖	mathematical	`IsOpen`	`IsGδ`	—	`Set.countable_singleton` `Set.sInter_singleton`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMeagre_image` 📖	mathematical	`Topology.IsInducing` `IsMeagre`	`Set.image`	—	`isMeagre_iff_countable_union_isNowhereDense` `isNowhereDense_image` `Set.Countable.image` `Set.image_sUnion` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `Set.image_mono` `subset_refl` `Set.instReflSubset`
`isNowhereDense_image` 📖	mathematical	`Topology.IsInducing` `IsNowhereDense`	`Set.image`	—	`isNowhereDense_iff_forall_notMem_nhds` `Set.forall_mem_image` `closure_eq_preimage_closure_image` `nhds_eq_comap` `Filter.preimage_mem_comap`

(root)

Definitions

Name	Category	Theorems
`IsGδ` 📖	MathDef	22 math math: `eventually_residual`, `Finset.isGδ_compl`, `IsGδ.biInter_of_isOpen`, `IsGδ.univ`, `Set.Finite.isGδ`, `IsGδ.setOf_continuousAt`, `MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariant`, `IsGδ.setOf_irrational`, `IsGδ.compl_singleton`, `IsClosed.isGδ`, `mem_residual`, `IsGδ.singleton`, `Set.Finite.isGδ_compl`, `Set.Subsingleton.isGδ_compl`, `IsGδ.setOf_liouville`, `isGδ_iff_eq_iInter_nat`, `IsGδ.empty`, `PerfectlyNormalSpace.closed_gdelta`, `IsOpen.isGδ`, `Set.Countable.isGδ_compl`, `MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant`, `IsGδ.iInter_of_isOpen`
`IsMeagre` 📖	MathDef	7 math math: `IsMeagre.of_isSigmaCompact_null`, `IsNowhereDense.isMeagre`, `not_isMeagre_of_isOpen`, `IsMeagre.empty`, `not_isMeagre_of_mem_residual`, `isMeagre_iff_countable_union_isNowhereDense`, `not_isMeagre_of_isGδ_of_dense`
`IsNowhereDense` 📖	MathDef	7 math math: `isNowhereDense_iff_forall_notMem_nhds`, `IsNowhereDense.of_isClosed_null`, `isClosed_isNowhereDense_iff_compl`, `isNowhereDense_iff_disjoint`, `isNowhereDense_empty`, `IsClosed.isNowhereDense_iff`, `isMeagre_iff_countable_union_isNowhereDense`
`residual` 📖	CompOp	16 math math: `eventually_residual`, `eventually_residual_irrational`, `countableInterFilter_residual`, `Homeomorph.residual_map_eq`, `tendsto_residual_of_isOpenMap`, `Real.disjoint_residual_ae`, `MeasurableSet.residualEq_isOpen`, `residual_of_dense_open`, `closure_residualEq`, `mem_residual`, `BaireMeasurableSet.residualEq_isOpen`, `coborder_mem_residual`, `BaireMeasurableSet.iff_residualEq_isOpen`, `eventually_residual_liouville`, `residual_of_dense_Gδ`, `mem_residual_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableInterFilter_residual` 📖	mathematical	—	`CountableInterFilter` `residual`	—	`residual.eq_1`
`exists_of_not_isMeagre_biUnion` 📖	—	`IsMeagre` `Set.iUnion` `Set` `Set.instMembership`	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `isMeagre_biUnion`
`isClosed_isNowhereDense_iff_compl` 📖	mathematical	—	`IsClosed` `IsNowhereDense` `IsOpen` `Compl.compl` `Set` `Set.instCompl` `Dense`	—	`IsClosed.isNowhereDense_iff` `isOpen_compl_iff` `interior_eq_empty_iff_dense_compl`
`isGδ_iff_eq_iInter_nat` 📖	mathematical	—	`IsGδ` `IsOpen` `Set.iInter`	—	`Set.eq_empty_or_nonempty` `isOpen_univ` `Set.sInter_empty` `Set.iInter_univ` `Set.Countable.exists_eq_range` `IsGδ.iInter_of_isOpen` `instCountableNat`
`isGδ_induced` 📖	mathematical	`Continuous` `IsGδ`	`Set.preimage`	—	`IsGδ.eq_iInter_nat` `Set.preimage_iInter` `IsGδ.iInter_of_isOpen` `instCountableNat` `Continuous.isOpen_preimage`
`isMeagre_biUnion` 📖	mathematical	`IsMeagre`	`Set.iUnion` `Set` `Set.instMembership`	—	`isMeagre_iUnion` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop`
`isMeagre_iUnion` 📖	mathematical	`IsMeagre`	`Set.iUnion`	—	`IsMeagre.eq_1` `Set.compl_iUnion` `countable_iInter_mem` `countableInterFilter_residual`
`isMeagre_iff_countable_union_isNowhereDense` 📖	mathematical	—	`IsMeagre` `IsNowhereDense` `Set.Countable` `Set` `Set.instHasSubset` `Set.sUnion`	—	`IsMeagre.eq_1` `mem_residual_iff` `Function.Surjective.exists` `Function.Surjective.image_surjective` `Function.Bijective.surjective` `compl_bijective` `Set.sInter_image` `Set.compl_compl_image` `Set.Countable.image` `Set.forall_mem_image` `isClosed_closure` `IsNowhereDense.closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.sUnion_mono_subsets` `subset_closure`
`isNowhereDense_empty` 📖	mathematical	—	`IsNowhereDense` `Set` `Set.instEmptyCollection`	—	`IsNowhereDense.eq_1` `closure_empty` `interior_empty`
`isNowhereDense_iff_disjoint` 📖	mathematical	—	`IsNowhereDense` `Disjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `interior` `closure`	—	`Set.disjoint_empty` `Disjoint.eq_bot_of_self` `Disjoint.mono_left` `interior_subset` `Disjoint.closure_left` `isOpen_interior`
`isNowhereDense_iff_forall_notMem_nhds` 📖	mathematical	—	`IsNowhereDense` `Set` `Filter` `Filter.instMembership` `nhds` `closure`	—	—
`mem_residual_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `residual` `IsOpen` `Dense` `Set.Countable` `Set.instHasSubset` `Set.sInter`	—	`Filter.mem_countableGenerate_iff`
`nonempty_of_not_isMeagre` 📖	mathematical	`IsMeagre`	`Set.Nonempty`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `IsMeagre.empty`
`residual_of_dense_Gδ` 📖	mathematical	`IsGδ` `Dense`	`Set` `Filter` `Filter.instMembership` `residual`	—	`countable_sInter_mem` `countableInterFilter_residual` `residual_of_dense_open` `Dense.mono` `Set.sInter_subset_of_mem`
`residual_of_dense_open` 📖	mathematical	`IsOpen` `Dense`	`Set` `Filter` `Filter.instMembership` `residual`	—	—

---

← Back to Index