Documentation Verification Report

Residual

📁 Source: Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean

Statistics

Metric	Count
Definitions	0
Theorems `setOf_liouville`, `dense_liouville`, `eventually_residual_liouville`, `setOf_liouville_eq_iInter_iUnion`, `setOf_liouville_eq_irrational_inter_iInter_iUnion`	5
Total	5

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`setOf_liouville` 📖	mathematical	—	`IsGδ` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Liouville`	—	`setOf_liouville_eq_iInter_iUnion` `iInter` `instCountableNat` `IsOpen.isGδ` `isOpen_iUnion` `IsOpen.inter` `Metric.isOpen_ball` `IsClosed.isOpen_compl` `isClosed_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_liouville` 📖	mathematical	—	`Dense` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Liouville`	—	`dense_of_mem_residual` `BaireSpace.of_t2Space_locallyCompactSpace` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `locallyCompact_of_proper` `instProperSpaceReal` `eventually_residual_liouville`
`eventually_residual_liouville` 📖	mathematical	—	`Filter.Eventually` `Real` `Liouville` `residual` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Filter.Eventually.eq_1` `setOf_liouville_eq_irrational_inter_iInter_iUnion` `Filter.Eventually.and` `eventually_residual_irrational` `residual_of_dense_Gδ` `IsGδ.iInter` `instCountableNat` `IsOpen.isGδ` `isOpen_iUnion` `Metric.isOpen_ball` `Dense.mono` `Rat.pos` `Nat.instAtLeastTwoHAddOfNat` `Int.cast_mul` `Int.cast_ofNat` `Int.cast_natCast` `Nat.cast_mul` `RCLike.charZero_rclike` `two_ne_zero` `Metric.mem_ball_self` `one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `Real.instZeroLEOneClass` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NeZero.charZero_one` `mul_pos` `Int.instIsStrictOrderedRing` `zero_lt_two` `Int.instZeroLEOneClass` `Int.instAddLeftMono` `IsDenseInducing.dense` `IsDenseEmbedding.toIsDenseInducing` `Rat.isDenseEmbedding_coe_real`
`setOf_liouville_eq_iInter_iUnion` 📖	mathematical	—	`setOf` `Real` `Liouville` `Set.iInter` `Set.iUnion` `Set` `Set.instSDiff` `Metric.ball` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Set.instSingletonSet`	—	`Set.ext`
`setOf_liouville_eq_irrational_inter_iInter_iUnion` 📖	mathematical	—	`setOf` `Real` `Liouville` `Set` `Set.instInter` `Irrational` `Set.iInter` `Set.iUnion` `Metric.ball` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid`	—	`Set.Subset.antisymm` `Set.subset_inter` `Liouville.irrational` `setOf_liouville_eq_iInter_iUnion` `Set.iInter_mono` `Set.iUnion₂_mono` `Set.iUnion_mono` `Set.diff_subset` `Set.inter_iInter` `Set.inter_iUnion` `Set.inter_comm` `Set.diff_subset_diff` `Set.Subset.rfl` `Set.singleton_subset_iff` `Rat.instCharZero` `RCLike.charZero_rclike`

---

← Back to Index