Commit 2023-10-26 21:10 b8e38026

View on Github →

feat: Sublattices (#7549) Basic API for sublattices (there's more to come).

Estimated changes

added theorem Sublattice.coe_bot
added theorem Sublattice.coe_comap
added theorem Sublattice.coe_copy
added theorem Sublattice.coe_eq_univ
added theorem Sublattice.coe_iInf
added theorem Sublattice.coe_inf'
added theorem Sublattice.coe_inf
added theorem Sublattice.coe_inj
added theorem Sublattice.coe_map
added theorem Sublattice.coe_mk
added theorem Sublattice.coe_sInf
added theorem Sublattice.coe_subtype
added theorem Sublattice.coe_sup
added theorem Sublattice.coe_top
added def Sublattice.comap
added theorem Sublattice.comap_comap
added theorem Sublattice.comap_iInf
added theorem Sublattice.comap_id
added theorem Sublattice.comap_inf
added theorem Sublattice.comap_mono
added theorem Sublattice.comap_top
added theorem Sublattice.copy_eq
added theorem Sublattice.ext
added theorem Sublattice.infClosed
added def Sublattice.map
added theorem Sublattice.map_bot
added theorem Sublattice.map_iSup
added theorem Sublattice.map_id
added theorem Sublattice.map_inf
added theorem Sublattice.map_inf_le
added theorem Sublattice.map_map
added theorem Sublattice.map_mono
added theorem Sublattice.map_sup
added theorem Sublattice.map_top
added theorem Sublattice.mem_carrier
added theorem Sublattice.mem_comap
added theorem Sublattice.mem_iInf
added theorem Sublattice.mem_inf
added theorem Sublattice.mem_map
added theorem Sublattice.mem_mk
added theorem Sublattice.mem_sInf
added theorem Sublattice.mem_top
added theorem Sublattice.mk_inf_mk
added theorem Sublattice.mk_le_mk
added theorem Sublattice.mk_lt_mk
added theorem Sublattice.mk_sup_mk
added theorem Sublattice.not_mem_bot
added theorem Sublattice.supClosed
added structure Sublattice