Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-26 21:10
b8e38026
View on Github →
feat: Sublattices (
#7549
) Basic API for sublattices (there's more to come).
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Order/Sublattice.lean
added
theorem
Sublattice.apply_coe_mem_map
added
theorem
Sublattice.apply_mem_map_iff
added
theorem
Sublattice.coe_bot
added
theorem
Sublattice.coe_comap
added
theorem
Sublattice.coe_copy
added
theorem
Sublattice.coe_eq_empty
added
theorem
Sublattice.coe_eq_univ
added
theorem
Sublattice.coe_iInf
added
theorem
Sublattice.coe_inclusion
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_equiv_eq_map_symm
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.gc_map_comap
added
def
Sublattice.inclusion
added
theorem
Sublattice.inclusion_apply
added
theorem
Sublattice.inclusion_injective
added
theorem
Sublattice.inclusion_rfl
added
theorem
Sublattice.infClosed
added
theorem
Sublattice.isSublattice
added
theorem
Sublattice.le_comap_iSup
added
theorem
Sublattice.le_comap_sup
added
def
Sublattice.map
added
theorem
Sublattice.map_bot
added
theorem
Sublattice.map_equiv_eq_comap_symm
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_le_iff_le_comap
added
theorem
Sublattice.map_map
added
theorem
Sublattice.map_mono
added
theorem
Sublattice.map_sup
added
theorem
Sublattice.map_symm_eq_iff_eq_map
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_map_equiv
added
theorem
Sublattice.mem_map_of_mem
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.subsingleton_iff
added
def
Sublattice.subtype
added
theorem
Sublattice.subtype_apply
added
theorem
Sublattice.subtype_comp_inclusion
added
theorem
Sublattice.subtype_injective
added
theorem
Sublattice.supClosed
added
def
Sublattice.topEquiv
added
structure
Sublattice