Commit 2023-03-17 12:26 f4d25055

View on Github →

feat: port Topology.Algebra.OpenSubgroup (#2889)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/OpenSubgroup.lean

added theorem Ideal.isOpen_of_open_subideal

added structure OpenAddSubgroup

added theorem OpenSubgroup.coe_comap

added theorem OpenSubgroup.coe_inf

added theorem OpenSubgroup.coe_prod

added theorem OpenSubgroup.coe_toOpens

added theorem OpenSubgroup.coe_toSubgroup

added theorem OpenSubgroup.coe_top

added def OpenSubgroup.comap

added theorem OpenSubgroup.comap_comap

added theorem OpenSubgroup.ext

added theorem OpenSubgroup.isClopen

added theorem OpenSubgroup.isClosed

added theorem OpenSubgroup.mem_comap

added theorem OpenSubgroup.mem_inf

added theorem OpenSubgroup.mem_nhds_one

added theorem OpenSubgroup.mem_toOpens

added theorem OpenSubgroup.mem_toSubgroup

added theorem OpenSubgroup.mem_top

added def OpenSubgroup.prod

added def OpenSubgroup.toOpens

added theorem OpenSubgroup.toOpens_inf

added theorem OpenSubgroup.toOpens_top

added theorem OpenSubgroup.toSubgroup_comap

added theorem OpenSubgroup.toSubgroup_inf

added theorem OpenSubgroup.toSubgroup_injective

added theorem OpenSubgroup.toSubgroup_le

added theorem OpenSubgroup.toSubgroup_prod

added theorem OpenSubgroup.toSubgroup_sup

added theorem OpenSubgroup.toSubgroup_top

added structure OpenSubgroup

added theorem Subgroup.isOpen_mono

added theorem Subgroup.isOpen_of_mem_nhds

added theorem Subgroup.isOpen_of_one_mem_interior

added theorem Subgroup.isOpen_of_openSubgroup

added theorem Submodule.isOpen_mono