Commit 2024-02-15 19:01 2be6479c

View on Github →

chore(Topology/GDelta): use new-style dot notation (#10583) Rename many isGδ_some lemmas to IsGδ.some. Also resolve a TODO.

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Measure/EverywherePos.lean

Modified Mathlib/NumberTheory/Liouville/Residual.lean

added theorem IsGδ.setOf_liouville

deleted theorem isGδ_setOf_liouville

Modified Mathlib/Topology/GDelta.lean

modified theorem IsClosed.isGδ

added theorem IsGδ.biInter

added theorem IsGδ.biInter_of_isOpen

added theorem IsGδ.biUnion

added theorem IsGδ.compl_singleton

added theorem IsGδ.iInter_of_isOpen

added theorem IsGδ.iUnion

added theorem IsGδ.sInter

added theorem IsGδ.sUnion

added theorem IsGδ.setOf_continuousAt

deleted theorem isGδ_biInter

deleted theorem isGδ_biInter_of_isOpen

deleted theorem isGδ_biUnion

deleted theorem isGδ_compl_singleton

deleted theorem isGδ_empty

deleted theorem isGδ_iInter

deleted theorem isGδ_iInter_of_isOpen

deleted theorem isGδ_sInter

deleted theorem isGδ_setOf_continuousAt

deleted theorem isGδ_singleton

deleted theorem isGδ_univ

Modified Mathlib/Topology/Instances/Irrational.lean

deleted theorem isGδ_irrational

Modified Mathlib/Topology/MetricSpace/Baire.lean