Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 07:59 c2fde701

View on Github →

feat(number_theory/liouville): Liouville numbers form a dense Gδ set (#9646)

Estimated changes

Created src/number_theory/liouville/residual.lean

added theorem dense_irrational

added theorem dense_liouville

added theorem eventually_residual_irrational

added theorem eventually_residual_liouville

added theorem is_Gδ_irrational

added theorem is_Gδ_set_of_liouville

added theorem set_of_liouville_eq_Inter_Union

added theorem set_of_liouville_eq_irrational_inter_Inter_Union

Modified src/topology/metric_space/baire.lean

added theorem dense_of_mem_residual