Commit 2024-12-18 18:00 b0466d1f

View on Github →

feat: boolean subalgebras (#20019) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/BooleanSubalgebra.lean

added theorem BooleanSubalgebra.apply_coe_mem_map

added theorem BooleanSubalgebra.apply_mem_map_iff

added theorem BooleanSubalgebra.biInf_mem

added theorem BooleanSubalgebra.biSup_mem

added theorem BooleanSubalgebra.bot_mem

added def BooleanSubalgebra.closure

added theorem BooleanSubalgebra.closure_bot_sup_induction

added theorem BooleanSubalgebra.closure_le

added theorem BooleanSubalgebra.closure_mono

added theorem BooleanSubalgebra.coe_bot

added theorem BooleanSubalgebra.coe_comap

added theorem BooleanSubalgebra.coe_copy

added theorem BooleanSubalgebra.coe_eq_univ

added theorem BooleanSubalgebra.coe_iInf

added theorem BooleanSubalgebra.coe_inclusion

added theorem BooleanSubalgebra.coe_inf

added theorem BooleanSubalgebra.coe_inj

added theorem BooleanSubalgebra.coe_map

added theorem BooleanSubalgebra.coe_mk

added theorem BooleanSubalgebra.coe_sInf

added theorem BooleanSubalgebra.coe_subtype

added theorem BooleanSubalgebra.coe_top

added def BooleanSubalgebra.comap

added theorem BooleanSubalgebra.comap_comap

added theorem BooleanSubalgebra.comap_equiv_eq_map_symm

added theorem BooleanSubalgebra.comap_iInf

added theorem BooleanSubalgebra.comap_id

added theorem BooleanSubalgebra.comap_inf

added theorem BooleanSubalgebra.comap_mono

added theorem BooleanSubalgebra.comap_top

added theorem BooleanSubalgebra.compl_mem

added theorem BooleanSubalgebra.compl_mem_iff

added theorem BooleanSubalgebra.compl_mk

added theorem BooleanSubalgebra.copy_eq

added theorem BooleanSubalgebra.ext

added theorem BooleanSubalgebra.gc_map_comap

added theorem BooleanSubalgebra.himp_mem

added theorem BooleanSubalgebra.iInf_mem

added theorem BooleanSubalgebra.iSup_mem

added def BooleanSubalgebra.inclusion

added theorem BooleanSubalgebra.inclusion_apply

added theorem BooleanSubalgebra.inclusion_injective

added theorem BooleanSubalgebra.inclusion_rfl

added theorem BooleanSubalgebra.infClosed

added theorem BooleanSubalgebra.inf_mem

added theorem BooleanSubalgebra.le_comap_iSup

added theorem BooleanSubalgebra.le_comap_sup

added def BooleanSubalgebra.map

added theorem BooleanSubalgebra.map_bot

added theorem BooleanSubalgebra.map_equiv_eq_comap_symm

added theorem BooleanSubalgebra.map_iSup

added theorem BooleanSubalgebra.map_id

added theorem BooleanSubalgebra.map_inf

added theorem BooleanSubalgebra.map_inf_le

added theorem BooleanSubalgebra.map_le_iff_le_comap

added theorem BooleanSubalgebra.map_map

added theorem BooleanSubalgebra.map_mono

added theorem BooleanSubalgebra.map_sup

added theorem BooleanSubalgebra.map_symm_eq_iff_eq_map

added theorem BooleanSubalgebra.map_top

added theorem BooleanSubalgebra.mem_bot

added theorem BooleanSubalgebra.mem_carrier

added theorem BooleanSubalgebra.mem_closure

added theorem BooleanSubalgebra.mem_comap

added theorem BooleanSubalgebra.mem_iInf

added theorem BooleanSubalgebra.mem_inf

added theorem BooleanSubalgebra.mem_map

added theorem BooleanSubalgebra.mem_map_equiv

added theorem BooleanSubalgebra.mem_map_of_mem

added theorem BooleanSubalgebra.mem_mk

added theorem BooleanSubalgebra.mem_sInf

added theorem BooleanSubalgebra.mem_toSublattice

added theorem BooleanSubalgebra.mem_top

added theorem BooleanSubalgebra.mk_bot

added theorem BooleanSubalgebra.mk_himp_mk

added theorem BooleanSubalgebra.mk_inf_mk

added theorem BooleanSubalgebra.mk_le_mk

added theorem BooleanSubalgebra.mk_lt_mk{L

added theorem BooleanSubalgebra.mk_sdiff_mk

added theorem BooleanSubalgebra.mk_sup_mk

added theorem BooleanSubalgebra.mk_top

added theorem BooleanSubalgebra.sInf_mem

added theorem BooleanSubalgebra.sSup_mem

added theorem BooleanSubalgebra.sdiff_mem

added theorem BooleanSubalgebra.subset_closure

added def BooleanSubalgebra.subtype

added theorem BooleanSubalgebra.subtype_apply

added theorem BooleanSubalgebra.subtype_comp_inclusion

added theorem BooleanSubalgebra.subtype_injective

added theorem BooleanSubalgebra.supClosed

added theorem BooleanSubalgebra.sup_mem

added def BooleanSubalgebra.topEquiv

added theorem BooleanSubalgebra.top_mem

added theorem BooleanSubalgebra.val_bot

added theorem BooleanSubalgebra.val_compl

added theorem BooleanSubalgebra.val_himp

added theorem BooleanSubalgebra.val_inf

added theorem BooleanSubalgebra.val_sdiff

added theorem BooleanSubalgebra.val_sup

added theorem BooleanSubalgebra.val_top

added structure BooleanSubalgebra

Modified Mathlib/Order/Sublattice.lean

added theorem Sublattice.inf_mem

added theorem Sublattice.sup_mem