Commit 2023-02-01 07:36 d869cdc9

View on Github →

feat: port Order.UpperLower.Basic (#1978)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/UpperLower/Basic.lean

added theorem IsLowerSet.bot_mem

added theorem IsLowerSet.compl

added theorem IsLowerSet.image

added theorem IsLowerSet.inter

added theorem IsLowerSet.not_bddBelow

added theorem IsLowerSet.not_bot_mem

added theorem IsLowerSet.ordConnected

added theorem IsLowerSet.preimage

added theorem IsLowerSet.prod

added theorem IsLowerSet.top_mem

added theorem IsLowerSet.union

added def IsLowerSet

added theorem IsUpperSet.bot_mem

added theorem IsUpperSet.compl

added theorem IsUpperSet.image

added theorem IsUpperSet.inter

added theorem IsUpperSet.not_bddAbove

added theorem IsUpperSet.not_top_mem

added theorem IsUpperSet.ordConnected

added theorem IsUpperSet.preimage

added theorem IsUpperSet.prod

added theorem IsUpperSet.top_mem

added theorem IsUpperSet.union

added def IsUpperSet

added theorem LowerSet.Ici_prod_Ici

added theorem LowerSet.Iic_inf

added theorem LowerSet.Iic_infᵢ

added theorem LowerSet.Iic_infᵢ₂

added theorem LowerSet.Iic_infₛ

added theorem LowerSet.Iic_prod

added theorem LowerSet.Ioi_le_Ici

added theorem LowerSet.bot_prod

added theorem LowerSet.carrier_eq_coe

added theorem LowerSet.coe_Iic

added theorem LowerSet.coe_Iio

added theorem LowerSet.coe_bot

added theorem LowerSet.coe_compl

added theorem LowerSet.coe_eq_empty

added theorem LowerSet.coe_eq_univ

added theorem LowerSet.coe_inf

added theorem LowerSet.coe_infᵢ

added theorem LowerSet.coe_infᵢ₂

added theorem LowerSet.coe_infₛ

added theorem LowerSet.coe_map

added theorem LowerSet.coe_prod

added theorem LowerSet.coe_subset_coe

added theorem LowerSet.coe_sup

added theorem LowerSet.coe_supᵢ

added theorem LowerSet.coe_supᵢ₂

added theorem LowerSet.coe_supₛ

added theorem LowerSet.coe_top

added def LowerSet.compl

added theorem LowerSet.compl_infᵢ₂

added theorem LowerSet.compl_le_compl

added theorem LowerSet.compl_map

added theorem LowerSet.compl_supᵢ₂

added theorem LowerSet.disjoint_coe

added theorem LowerSet.disjoint_prod

added theorem LowerSet.ext

added theorem LowerSet.inf_prod

added def LowerSet.map

added theorem LowerSet.map_Iic

added theorem LowerSet.map_Iio

added theorem LowerSet.map_map

added theorem LowerSet.map_refl

added theorem LowerSet.mem_Iic_iff

added theorem LowerSet.mem_Iio_iff

added theorem LowerSet.mem_compl_iff

added theorem LowerSet.mem_inf_iff

added theorem LowerSet.mem_infᵢ_iff

added theorem LowerSet.mem_infᵢ₂_iff

added theorem LowerSet.mem_infₛ_iff

added theorem LowerSet.mem_map

added theorem LowerSet.mem_mk

added theorem LowerSet.mem_prod

added theorem LowerSet.mem_sup_iff

added theorem LowerSet.mem_supᵢ_iff

added theorem LowerSet.mem_supᵢ₂_iff

added theorem LowerSet.mem_supₛ_iff

added theorem LowerSet.mem_top

added theorem LowerSet.not_mem_bot

added def LowerSet.prod

added theorem LowerSet.prod_bot

added theorem LowerSet.prod_eq_bot

added theorem LowerSet.prod_inf

added theorem LowerSet.prod_inf_prod

added theorem LowerSet.prod_le_prod_iff

added theorem LowerSet.prod_mono

added theorem LowerSet.prod_mono_left

added theorem LowerSet.prod_mono_right

added theorem LowerSet.prod_self_le_prod_self

added theorem LowerSet.prod_self_lt_prod_self

added theorem LowerSet.prod_sup

added theorem LowerSet.sup_prod

added theorem LowerSet.supᵢ_Iic

added theorem LowerSet.symm_map

added theorem LowerSet.top_prod_top

added structure LowerSet

added theorem Set.OrdConnected.upperClosure_inter_lowerClosure

added theorem Set.antitone_mem

added theorem Set.monotone_mem

added theorem UpperSet.Ici_le_Ioi

added theorem UpperSet.Ici_prod

added theorem UpperSet.Ici_prod_Ici

added theorem UpperSet.Ici_sup

added theorem UpperSet.Ici_supᵢ

added theorem UpperSet.Ici_supᵢ₂

added theorem UpperSet.Ici_supₛ

added theorem UpperSet.bot_prod_bot

added theorem UpperSet.carrier_eq_coe

added theorem UpperSet.codisjoint_coe

added theorem UpperSet.codisjoint_prod

added theorem UpperSet.coe_Ici

added theorem UpperSet.coe_Ioi

added theorem UpperSet.coe_bot

added theorem UpperSet.coe_compl

added theorem UpperSet.coe_eq_empty

added theorem UpperSet.coe_eq_univ

added theorem UpperSet.coe_inf

added theorem UpperSet.coe_infᵢ

added theorem UpperSet.coe_infᵢ₂

added theorem UpperSet.coe_infₛ

added theorem UpperSet.coe_map

added theorem UpperSet.coe_prod

added theorem UpperSet.coe_subset_coe

added theorem UpperSet.coe_sup

added theorem UpperSet.coe_supᵢ

added theorem UpperSet.coe_supᵢ₂

added theorem UpperSet.coe_supₛ

added theorem UpperSet.coe_top

added def UpperSet.compl

added theorem UpperSet.compl_infᵢ₂

added theorem UpperSet.compl_le_compl

added theorem UpperSet.compl_map

added theorem UpperSet.compl_supᵢ₂

added theorem UpperSet.ext

added theorem UpperSet.inf_prod

added theorem UpperSet.infᵢ_Ici

added def UpperSet.map

added theorem UpperSet.map_Ici

added theorem UpperSet.map_Ioi

added theorem UpperSet.map_map

added theorem UpperSet.map_refl

added theorem UpperSet.mem_Ici_iff

added theorem UpperSet.mem_Ioi_iff

added theorem UpperSet.mem_bot

added theorem UpperSet.mem_compl_iff

added theorem UpperSet.mem_inf_iff

added theorem UpperSet.mem_infᵢ_iff

added theorem UpperSet.mem_infᵢ₂_iff

added theorem UpperSet.mem_infₛ_iff

added theorem UpperSet.mem_map

added theorem UpperSet.mem_mk

added theorem UpperSet.mem_prod

added theorem UpperSet.mem_sup_iff

added theorem UpperSet.mem_supᵢ_iff

added theorem UpperSet.mem_supᵢ₂_iff

added theorem UpperSet.mem_supₛ_iff

added theorem UpperSet.not_mem_top

added def UpperSet.prod

added theorem UpperSet.prod_eq_top

added theorem UpperSet.prod_inf

added theorem UpperSet.prod_le_prod_iff

added theorem UpperSet.prod_mono

added theorem UpperSet.prod_mono_left

added theorem UpperSet.prod_mono_right

added theorem UpperSet.prod_self_le_prod_self

added theorem UpperSet.prod_self_lt_prod_self

added theorem UpperSet.prod_sup

added theorem UpperSet.prod_sup_prod

added theorem UpperSet.prod_top

added theorem UpperSet.sup_prod

added theorem UpperSet.symm_map

added theorem UpperSet.top_prod

added structure UpperSet

added theorem coe_lowerClosure

added theorem coe_upperClosure

added theorem gc_lowerClosure_coe

added theorem gc_upperClosure_coe

added def giLowerClosureCoe

added def giUpperClosureCoe

added theorem isLowerSet_Iic

added theorem isLowerSet_Iio

added theorem isLowerSet_compl

added theorem isLowerSet_empty

added theorem isLowerSet_iff_Iic_subset

added theorem isLowerSet_iff_Iio_subset

added theorem isLowerSet_iff_forall_lt

added theorem isLowerSet_interᵢ

added theorem isLowerSet_interᵢ₂

added theorem isLowerSet_interₛ

added theorem isLowerSet_preimage_ofDual_iff

added theorem isLowerSet_preimage_toDual_iff

added theorem isLowerSet_setOf

added theorem isLowerSet_unionᵢ

added theorem isLowerSet_unionᵢ₂

added theorem isLowerSet_unionₛ

added theorem isLowerSet_univ

added theorem isUpperSet_Ici

added theorem isUpperSet_Ioi

added theorem isUpperSet_compl

added theorem isUpperSet_empty

added theorem isUpperSet_iff_Ici_subset

added theorem isUpperSet_iff_Ioi_subset

added theorem isUpperSet_iff_forall_lt

added theorem isUpperSet_interᵢ

added theorem isUpperSet_interᵢ₂

added theorem isUpperSet_interₛ

added theorem isUpperSet_preimage_ofDual_iff

added theorem isUpperSet_preimage_toDual_iff

added theorem isUpperSet_setOf

added theorem isUpperSet_unionᵢ

added theorem isUpperSet_unionᵢ₂

added theorem isUpperSet_unionₛ

added theorem isUpperSet_univ

added def lowerClosure

added theorem lowerClosure_empty

added theorem lowerClosure_eq_bot_iff

added theorem lowerClosure_image

added theorem lowerClosure_min

added theorem lowerClosure_mono

added theorem lowerClosure_prod

added theorem lowerClosure_singleton

added theorem lowerClosure_union

added theorem lowerClosure_unionᵢ

added theorem lowerClosure_unionₛ

added theorem lowerClosure_univ

added theorem mem_lowerClosure

added theorem mem_upperClosure

added theorem not_bddAbove_Ici

added theorem not_bddAbove_Ioi

added theorem not_bddBelow_Iic

added theorem not_bddBelow_Iio

added theorem ordConnected_iff_upperClosure_inter_lowerClosure

added theorem subset_lowerClosure

added theorem subset_upperClosure

added def upperClosure

added theorem upperClosure_anti

added theorem upperClosure_empty

added theorem upperClosure_eq_top_iff

added theorem upperClosure_image

added theorem upperClosure_min

added theorem upperClosure_prod

added theorem upperClosure_singleton

added theorem upperClosure_union

added theorem upperClosure_unionᵢ

added theorem upperClosure_unionₛ

added theorem upperClosure_univ

added def upperSetIsoLowerSet