Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-18 17:14 546618eb

View on Github →

feat(order/upper_lower): Principal upper/lower sets (#13069) Define upper_set.Ici and lower_set.Iic. Also add membership lemmas for the lattice operations.

Estimated changes

added theorem set.Ici_Sup
added theorem set.Ici_supr
added theorem set.Ici_supr₂
added theorem set.Iic_Inf
added theorem set.Iic_infi
added theorem set.Iic_infi₂
added theorem is_lower_set_Iic
added theorem is_lower_set_Iio
added theorem is_upper_set_Ici
added theorem is_upper_set_Ioi
added def lower_set.Iic
added theorem lower_set.Iic_Inf
added theorem lower_set.Iic_inf
added theorem lower_set.Iic_infi
added theorem lower_set.Iic_infi₂
added theorem lower_set.Iic_top
added def lower_set.Iio
added theorem lower_set.Iio_bot
added theorem lower_set.Ioi_le_Ici
added theorem lower_set.coe_Iic
added theorem lower_set.coe_Iio
added theorem lower_set.mem_Iic_iff
added theorem lower_set.mem_Iio_iff
added theorem lower_set.mem_Inf_iff
added theorem lower_set.mem_Sup_iff
added theorem lower_set.mem_inf_iff
added theorem lower_set.mem_infi_iff
added theorem lower_set.mem_sup_iff
added theorem lower_set.mem_supr_iff
added theorem lower_set.mem_top
added theorem lower_set.not_mem_bot
added def upper_set.Ici
added theorem upper_set.Ici_Sup
added theorem upper_set.Ici_sup
added theorem upper_set.Ici_supr
added theorem upper_set.Ici_supr₂
added theorem upper_set.Ici_top
added def upper_set.Ioi
added theorem upper_set.Ioi_bot
added theorem upper_set.Ioi_le_Ici
added theorem upper_set.coe_Ici
added theorem upper_set.coe_Ioi
added theorem upper_set.mem_Ici_iff
added theorem upper_set.mem_Inf_iff
added theorem upper_set.mem_Ioi_iff
added theorem upper_set.mem_Sup_iff
added theorem upper_set.mem_inf_iff
added theorem upper_set.mem_infi_iff
added theorem upper_set.mem_sup_iff
added theorem upper_set.mem_supr_iff
added theorem upper_set.mem_top
added theorem upper_set.not_mem_bot