Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-14 10:31 c5afc52a

View on Github →

feat(topology/metric_space/baire): Baire theorem (#816)

Estimated changes

Modified src/data/set/countable.lean

added theorem set.countable_prod

added theorem set.exists_surjective_of_countable

Modified src/data/set/lattice.lean

added theorem set.bInter_image

added theorem set.bInter_range

added theorem set.bUnion_image

added theorem set.bUnion_range

added theorem set.sInter_bUnion

added theorem set.sInter_range

added theorem set.sInter_union_sInter

added theorem set.sUnion_bUnion

added theorem set.sUnion_inter_sUnion

added theorem set.sUnion_range

Modified src/order/complete_boolean_algebra.lean

added theorem lattice.Inf_sup_Inf

added theorem lattice.Inf_sup_eq

added theorem lattice.Sup_inf_Sup

added theorem lattice.Sup_inf_eq

Modified src/order/complete_lattice.lean

added theorem lattice.infi_le_infi_of_subset

added theorem lattice.supr_le_supr_of_subset

Modified src/topology/basic.lean

added theorem interior_frontier

added theorem is_closed_frontier

Created src/topology/metric_space/baire.lean

added theorem dense_Inter_of_Gδ

added theorem dense_Inter_of_open

added theorem dense_Inter_of_open_nat

added theorem dense_Union_interior_of_closed

added theorem dense_bInter_of_Gδ

added theorem dense_bInter_of_open

added theorem dense_bUnion_interior_of_closed

added theorem dense_sInter_of_Gδ

added theorem dense_sInter_of_open

added theorem dense_sUnion_interior_of_closed

added theorem is_Gδ.union

added def is_Gδ

added theorem is_Gδ_Inter_of_open

added theorem is_Gδ_bInter_of_open

added theorem is_Gδ_sInter

added theorem is_open.is_Gδ

added theorem nonempty_interior_of_Union_of_closed

Modified src/topology/metric_space/basic.lean

added theorem metric.mem_closed_ball_self