Commit 2024-02-05 10:10 d27890e8

View on Github →

chore(MetricSpace/Baire): fix Encodable/Countable (#10249)

Assume {ι : Sort*} [Countable ι] instead of {ι : Type*} [Encodable ι].
Generalize 2nd Baire theorem from T₂ spaces to R₁ spaces.
Rename type variables.

Estimated changes

Modified Mathlib/Topology/MetricSpace/Baire.lean

modified theorem Dense.inter_of_Gδ

modified theorem IsGδ.dense_biUnion_interior_of_closed

modified theorem IsGδ.dense_iUnion_interior_of_closed

modified theorem IsGδ.dense_sUnion_interior_of_closed

modified theorem dense_biInter_of_Gδ

modified theorem dense_biInter_of_isOpen

modified theorem dense_biUnion_interior_of_closed

modified theorem dense_iInter_of_Gδ

modified theorem dense_iInter_of_isOpen

modified theorem dense_iInter_of_isOpen_nat

modified theorem dense_iUnion_interior_of_closed

modified theorem dense_of_mem_residual

modified theorem dense_sInter_of_Gδ

modified theorem dense_sInter_of_isOpen

modified theorem dense_sUnion_interior_of_closed

modified theorem eventually_residual

modified theorem mem_residual

modified theorem nonempty_interior_of_iUnion_of_closed

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem IsOpen.exists_positiveCompacts_closure_subset