Commit 2023-03-06 08:38 342815a1

View on Github →

feat: port Topology.Instances.Real (#2633) I generalized some lemmas from additive subgroups of the real numbers to additive subgroups of an archimedean additive group.

Estimated changes

modified theorem Int.subgroup_cyclic
added theorem abs_mem_iff
added theorem Filter.cofinite_eq_bot
modified theorem Rat.denseRange_cast
added theorem Real.Continuous.inv
added theorem Real.cocompact_eq
added theorem Real.continuous_inv
added theorem Real.mem_closure_iff
added theorem Real.tendsto_inv