Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-04 13:40 3ae6cea5

View on Github →

feat(group_theory/submonoid/operations): transfer galois connection/insertion lemmas (#3657)

Estimated changes

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.comap_id

added theorem submonoid.comap_inf_map_of_injective

added theorem submonoid.comap_infi_map_of_injective

added theorem submonoid.comap_injective_of_surjective

added theorem submonoid.comap_le_comap_iff_of_surjective

added theorem submonoid.comap_map_comap

added theorem submonoid.comap_map_eq_of_injective

added theorem submonoid.comap_strict_mono_of_surjective

added theorem submonoid.comap_sup_map_of_injective

added theorem submonoid.comap_supr_map_of_injective

added theorem submonoid.comap_surjective_of_injective

added def submonoid.gci_map_comap

added def submonoid.gi_map_comap

added theorem submonoid.le_comap_map

added theorem submonoid.le_comap_of_map_le

added theorem submonoid.map_comap_eq_of_surjective

added theorem submonoid.map_comap_le

added theorem submonoid.map_comap_map

added theorem submonoid.map_inf_comap_of_surjective

added theorem submonoid.map_infi_comap_of_surjective

added theorem submonoid.map_injective_of_injective

added theorem submonoid.map_le_map_iff_of_injective

added theorem submonoid.map_le_of_le_comap

added theorem submonoid.map_strict_mono_of_injective

added theorem submonoid.map_sup_comap_of_surjective

added theorem submonoid.map_supr_comap_of_surjective

added theorem submonoid.map_surjective_of_surjective

added theorem submonoid.monotone_comap

added theorem submonoid.monotone_map