Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 16:17 22bdc8ec

View on Github →

feat(order/upper_lower): Upper/lower sets (#12189) Define upper and lower sets both as unbundled predicates and as bundled types.

Estimated changes

Modified src/order/complete_boolean_algebra.lean

added theorem compl_Inf'

modified theorem compl_Inf

added theorem compl_Sup'

modified theorem compl_Sup

Created src/order/upper_lower.lean

added theorem is_lower_set.compl

added theorem is_lower_set.inter

added theorem is_lower_set.union

added def is_lower_set

added theorem is_lower_set_Inter

added theorem is_lower_set_Inter₂

added theorem is_lower_set_Union

added theorem is_lower_set_Union₂

added theorem is_lower_set_empty

added theorem is_lower_set_preimage_of_dual_iff

added theorem is_lower_set_preimage_to_dual_iff

added theorem is_lower_set_sInter

added theorem is_lower_set_sUnion

added theorem is_lower_set_univ

added theorem is_upper_set.compl

added theorem is_upper_set.inter

added theorem is_upper_set.union

added def is_upper_set

added theorem is_upper_set_Inter

added theorem is_upper_set_Inter₂

added theorem is_upper_set_Union

added theorem is_upper_set_Union₂

added theorem is_upper_set_empty

added theorem is_upper_set_preimage_of_dual_iff

added theorem is_upper_set_preimage_to_dual_iff

added theorem is_upper_set_sInter

added theorem is_upper_set_sUnion

added theorem is_upper_set_univ

added theorem lower_set.coe_Inf

added theorem lower_set.coe_Sup

added theorem lower_set.coe_bot

added theorem lower_set.coe_compl

added theorem lower_set.coe_inf

added theorem lower_set.coe_infi

added theorem lower_set.coe_infi₂

added theorem lower_set.coe_sup

added theorem lower_set.coe_supr

added theorem lower_set.coe_supr₂

added theorem lower_set.coe_top

added def lower_set.compl

added theorem lower_set.compl_compl

added theorem lower_set.compl_infi₂

added theorem lower_set.compl_supr₂

added theorem lower_set.ext

added structure lower_set

added theorem upper_set.coe_Inf

added theorem upper_set.coe_Sup

added theorem upper_set.coe_bot

added theorem upper_set.coe_compl

added theorem upper_set.coe_inf

added theorem upper_set.coe_infi

added theorem upper_set.coe_infi₂

added theorem upper_set.coe_sup

added theorem upper_set.coe_supr

added theorem upper_set.coe_supr₂

added theorem upper_set.coe_top

added def upper_set.compl

added theorem upper_set.compl_compl

added theorem upper_set.compl_infi₂

added theorem upper_set.compl_supr₂

added theorem upper_set.ext

added structure upper_set