Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 16:32 ec6d9a73

View on Github →

feat(topology/algebra/group): definitionally better lattice (#10792) This provides (⊓), ⊤, and ⊥ explicitly such that the associated to_topological_space lemmas are definitionally equal.

Estimated changes

Modified src/topology/algebra/group.lean

added theorem group_topology.continuous_inv'

added theorem group_topology.continuous_mul'

modified theorem group_topology.ext'

added theorem group_topology.to_topological_space_Inf

added theorem group_topology.to_topological_space_bot

added theorem group_topology.to_topological_space_inf

added theorem group_topology.to_topological_space_infi

added theorem group_topology.to_topological_space_injective

added theorem group_topology.to_topological_space_le

added theorem group_topology.to_topological_space_top

Modified src/topology/constructions.lean

added theorem continuous_Inf_dom₂

added theorem continuous_inf_dom_left₂

added theorem continuous_inf_dom_right₂